<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<link href="common/css/sf.css" rel="stylesheet" type="text/css" />
<title>Tactics: More Basic Tactics</title>
<link href="common/jquery-ui/jquery-ui.css" rel="stylesheet">
<script src="common/jquery-ui/external/jquery/jquery.js"></script>
<script src="common/jquery-ui/jquery-ui.js"></script>
<script src="common/toggleproofs.js"></script>
<link href="common/css/lf.css" rel="stylesheet" type="text/css"/>
</head>

<body>

<div id="page">

<div id="header">
<div id='logoinheader'><a href='https://softwarefoundations.cis.upenn.edu'>
<img src='common/media/image/sf_logo_sm.png' alt='Software Foundations Logo'></a></div>
<div class='booktitleinheader'><a href='index.html'>Volume 1: Logical Foundations</a></div>
<ul id='menu'>
   <li class='section_name'><a href='toc.html'>Table of Contents</a></li>
   <li class='section_name'><a href='coqindex.html'>Index</a></li>
   <li class='section_name'><a href='deps.html'>Roadmap</a></li>
</ul>
</div>

<div id="main">

<h1 class="libtitle">Tactics<span class="subtitle">More Basic Tactics</span></h1>

<div class="code">
</div>

<div class="doc">

<div class="paragraph"> </div>

 This chapter introduces several additional proof strategies
    and tactics that allow us to begin proving more interesting
    properties of functional programs.

<div class="paragraph"> </div>

    We will see:
<ul class="doclist">
<li> how to use auxiliary lemmas in both "forward-" and
      "backward-style" proofs;

</li>
<li> how to reason about data constructors -- in particular, how to
      use the fact that they are injective and disjoint;

</li>
<li> how to strengthen an induction hypothesis, and when such
      strengthening is required; and

</li>
<li> more details on how to reason by case analysis. 
</li>
</ul>

</div>
<div class="code">

<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">LF</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Export</span> <a class="idref" href="Poly.html#"><span class="id" title="library">Poly</span></a>.<br/>
</div>

<div class="doc">
<a id="lab139"></a><h1 class="section">The <span class="inlinecode"><span class="id" title="tactic">apply</span></span> Tactic</h1>

<div class="paragraph"> </div>

 We often encounter situations where the goal to be proved is
    <i>exactly</i> the same as some hypothesis in the context or some
    previously proved lemma. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Theorem</span> <a id="silly1" class="idref" href="#silly1"><span class="id" title="lemma">silly1</span></a> : <span class="id" title="keyword">∀</span> (<a id="n:1" class="idref" href="#n:1"><span class="id" title="binder">n</span></a> <a id="m:2" class="idref" href="#m:2"><span class="id" title="binder">m</span></a> <a id="o:3" class="idref" href="#o:3"><span class="id" title="binder">o</span></a> <a id="p:4" class="idref" href="#p:4"><span class="id" title="binder">p</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Tactics.html#n:1"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Tactics.html#m:2"><span class="id" title="variable">m</span></a>  <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Tactics.html#n:1"><span class="id" title="variable">n</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a><a class="idref" href="Tactics.html#o:3"><span class="id" title="variable">o</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Tactics.html#n:1"><span class="id" title="variable">n</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a><a class="idref" href="Tactics.html#p:4"><span class="id" title="variable">p</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Tactics.html#n:1"><span class="id" title="variable">n</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a><a class="idref" href="Tactics.html#o:3"><span class="id" title="variable">o</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Tactics.html#m:2"><span class="id" title="variable">m</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a><a class="idref" href="Tactics.html#p:4"><span class="id" title="variable">p</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">n</span> <span class="id" title="var">m</span> <span class="id" title="var">o</span> <span class="id" title="var">p</span> <span class="id" title="var">eq<sub>1</sub></span> <span class="id" title="var">eq<sub>2</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">rewrite</span> &lt;- <span class="id" title="var">eq<sub>1</sub></span>.<br/>
</div>

<div class="doc">
Here, we could finish with "<span class="inlinecode"><span class="id" title="tactic">rewrite</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" title="var">eq<sub>2</sub></span>.</span>  <span class="inlinecode"><span class="id" title="tactic">reflexivity</span>.</span>" as we
    have done several times before.  We can finish this proof in
    a single step by using the <span class="inlinecode"><span class="id" title="tactic">apply</span></span> tactic instead: 
</div>
<div class="code">

<br/>
&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <span class="id" title="var">eq<sub>2</sub></span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
The <span class="inlinecode"><span class="id" title="tactic">apply</span></span> tactic also works with <i>conditional</i> hypotheses
    and lemmas: if the statement being applied is an implication, then
    the premises of this implication will be added to the list of
    subgoals needing to be proved. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Theorem</span> <a id="silly2" class="idref" href="#silly2"><span class="id" title="lemma">silly2</span></a> : <span class="id" title="keyword">∀</span> (<a id="n:5" class="idref" href="#n:5"><span class="id" title="binder">n</span></a> <a id="m:6" class="idref" href="#m:6"><span class="id" title="binder">m</span></a> <a id="o:7" class="idref" href="#o:7"><span class="id" title="binder">o</span></a> <a id="p:8" class="idref" href="#p:8"><span class="id" title="binder">p</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Tactics.html#n:5"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Tactics.html#m:6"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">(</span></a><a class="idref" href="Tactics.html#n:5"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Tactics.html#m:6"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Tactics.html#n:5"><span class="id" title="variable">n</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a><a class="idref" href="Tactics.html#o:7"><span class="id" title="variable">o</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Tactics.html#m:6"><span class="id" title="variable">m</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a><a class="idref" href="Tactics.html#p:8"><span class="id" title="variable">p</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Tactics.html#n:5"><span class="id" title="variable">n</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a><a class="idref" href="Tactics.html#o:7"><span class="id" title="variable">o</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Tactics.html#m:6"><span class="id" title="variable">m</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a><a class="idref" href="Tactics.html#p:8"><span class="id" title="variable">p</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">n</span> <span class="id" title="var">m</span> <span class="id" title="var">o</span> <span class="id" title="var">p</span> <span class="id" title="var">eq<sub>1</sub></span> <span class="id" title="var">eq<sub>2</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <span class="id" title="var">eq<sub>2</sub></span>. <span class="id" title="tactic">apply</span> <span class="id" title="var">eq<sub>1</sub></span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
Typically, when we use <span class="inlinecode"><span class="id" title="tactic">apply</span></span> <span class="inlinecode"><span class="id" title="var">H</span></span>, the statement <span class="inlinecode"><span class="id" title="var">H</span></span> will
    begin with a <span class="inlinecode"><span class="id" title="keyword">∀</span></span> that introduces some <i>universally quantified
    variables</i>.  When Coq matches the current goal against the
    conclusion of <span class="inlinecode"><span class="id" title="var">H</span></span>, it will try to find appropriate values for
    these variables.  For example, when we do <span class="inlinecode"><span class="id" title="tactic">apply</span></span> <span class="inlinecode"><span class="id" title="var">eq<sub>2</sub></span></span> in the
    following proof, the universal variable <span class="inlinecode"><span class="id" title="var">q</span></span> in <span class="inlinecode"><span class="id" title="var">eq<sub>2</sub></span></span> gets
    instantiated with <span class="inlinecode"><span class="id" title="var">n</span></span>, and <span class="inlinecode"><span class="id" title="var">r</span></span> gets instantiated with <span class="inlinecode"><span class="id" title="var">m</span></span>. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Theorem</span> <a id="silly2a" class="idref" href="#silly2a"><span class="id" title="lemma">silly2a</span></a> : <span class="id" title="keyword">∀</span> (<a id="n:9" class="idref" href="#n:9"><span class="id" title="binder">n</span></a> <a id="m:10" class="idref" href="#m:10"><span class="id" title="binder">m</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="Tactics.html#n:9"><span class="id" title="variable">n</span></a><a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">,</span></a><a class="idref" href="Tactics.html#n:9"><span class="id" title="variable">n</span></a><a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="Tactics.html#m:10"><span class="id" title="variable">m</span></a><a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">,</span></a><a class="idref" href="Tactics.html#m:10"><span class="id" title="variable">m</span></a><a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">)</span></a>  <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">(</span></a><span class="id" title="keyword">∀</span> (<a id="q:11" class="idref" href="#q:11"><span class="id" title="binder">q</span></a> <a id="r:12" class="idref" href="#r:12"><span class="id" title="binder">r</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>), <a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="Tactics.html#q:11"><span class="id" title="variable">q</span></a><a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">,</span></a><a class="idref" href="Tactics.html#q:11"><span class="id" title="variable">q</span></a><a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="Tactics.html#r:12"><span class="id" title="variable">r</span></a><a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">,</span></a><a class="idref" href="Tactics.html#r:12"><span class="id" title="variable">r</span></a><a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Tactics.html#q:11"><span class="id" title="variable">q</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Tactics.html#r:12"><span class="id" title="variable">r</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Tactics.html#n:9"><span class="id" title="variable">n</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Tactics.html#m:10"><span class="id" title="variable">m</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">n</span> <span class="id" title="var">m</span> <span class="id" title="var">eq<sub>1</sub></span> <span class="id" title="var">eq<sub>2</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <span class="id" title="var">eq<sub>2</sub></span>. <span class="id" title="tactic">apply</span> <span class="id" title="var">eq<sub>1</sub></span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a id="lab140"></a><h4 class="section">Exercise: 2 stars, standard, optional (silly_ex)</h4>
 Complete the following proof using only <span class="inlinecode"><span class="id" title="tactic">intros</span></span> and <span class="inlinecode"><span class="id" title="tactic">apply</span></span>. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Theorem</span> <a id="silly_ex" class="idref" href="#silly_ex"><span class="id" title="lemma">silly_ex</span></a> :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">(</span></a><span class="id" title="keyword">∀</span> <a id="n:13" class="idref" href="#n:13"><span class="id" title="binder">n</span></a>, <a class="idref" href="Basics.html#evenb"><span class="id" title="definition">evenb</span></a> <a class="idref" href="Tactics.html#n:13"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Basics.html#oddb"><span class="id" title="definition">oddb</span></a> (<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <a class="idref" href="Tactics.html#n:13"><span class="id" title="variable">n</span></a>) <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Basics.html#evenb"><span class="id" title="definition">evenb</span></a> 2 <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Basics.html#oddb"><span class="id" title="definition">oddb</span></a> 3 <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

 To use the <span class="inlinecode"><span class="id" title="tactic">apply</span></span> tactic, the (conclusion of the) fact
    being applied must match the goal exactly -- for example, <span class="inlinecode"><span class="id" title="tactic">apply</span></span>
    will not work if the left and right sides of the equality are
    swapped. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Theorem</span> <a id="silly3_firsttry" class="idref" href="#silly3_firsttry"><span class="id" title="lemma">silly3_firsttry</span></a> : <span class="id" title="keyword">∀</span> (<a id="n:14" class="idref" href="#n:14"><span class="id" title="binder">n</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="Tactics.html#n:14"><span class="id" title="variable">n</span></a> <a class="idref" href="Basics.html#ad2ec4e405f68c46c0a176e3e94ae2e<sub>3</sub>"><span class="id" title="notation">=?</span></a> 5<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a>  <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Basics.html#ad2ec4e405f68c46c0a176e3e94ae2e<sub>3</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> (<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <a class="idref" href="Tactics.html#n:14"><span class="id" title="variable">n</span></a>)<a class="idref" href="Basics.html#ad2ec4e405f68c46c0a176e3e94ae2e<sub>3</sub>"><span class="id" title="notation">)</span></a> <a class="idref" href="Basics.html#ad2ec4e405f68c46c0a176e3e94ae2e<sub>3</sub>"><span class="id" title="notation">=?</span></a> 7 <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">n</span> <span class="id" title="var">H</span>.<br/>
</div>

<div class="doc">
Here we cannot use <span class="inlinecode"><span class="id" title="tactic">apply</span></span> directly, but we can use the <span class="inlinecode"><span class="id" title="tactic">symmetry</span></span>
    tactic, which switches the left and right sides of an equality in
    the goal. 
</div>
<div class="code">

<br/>
&nbsp;&nbsp;<span class="id" title="tactic">symmetry</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">simpl</span>. </div>

<div class="doc">
(This <span class="inlinecode"><span class="id" title="tactic">simpl</span></span> is optional, since <span class="inlinecode"><span class="id" title="tactic">apply</span></span> will perform
             simplification first, if needed.) 
</div>
<div class="code">
&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <span class="id" title="var">H</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a id="lab141"></a><h4 class="section">Exercise: 3 stars, standard (apply_exercise1)</h4>
 <i>Hint</i>: You can use <span class="inlinecode"><span class="id" title="tactic">apply</span></span> with previously defined lemmas, not
    just hypotheses in the context.  You may find earlier lemmas like
    <span class="inlinecode"><span class="id" title="var">app_nil_r</span></span>, <span class="inlinecode"><span class="id" title="var">app_assoc</span></span>, <span class="inlinecode"><span class="id" title="var">rev_app_distr</span></span>, <span class="inlinecode"><span class="id" title="var">rev_involutive</span></span>,
    etc. helpful.  Also, remember that <span class="inlinecode"><span class="id" title="keyword">Search</span></span> is your friend
    (though it may not find earlier lemmas if they were posed as
    optional problems and you chose not to finish the proofs). 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Theorem</span> <a id="rev_exercise1" class="idref" href="#rev_exercise1"><span class="id" title="lemma">rev_exercise1</span></a> : <span class="id" title="keyword">∀</span> (<a id="l:15" class="idref" href="#l:15"><span class="id" title="binder">l</span></a> <a id="l':16" class="idref" href="#l':16"><span class="id" title="binder">l'</span></a> : <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Tactics.html#l:15"><span class="id" title="variable">l</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#rev"><span class="id" title="definition">rev</span></a> <a class="idref" href="Tactics.html#l':16"><span class="id" title="variable">l'</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Tactics.html#l':16"><span class="id" title="variable">l'</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#rev"><span class="id" title="definition">rev</span></a> <a class="idref" href="Tactics.html#l:15"><span class="id" title="variable">l</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

<a id="lab142"></a><h4 class="section">Exercise: 1 star, standard, optional (apply_rewrite)</h4>
 Briefly explain the difference between the tactics <span class="inlinecode"><span class="id" title="tactic">apply</span></span> and
    <span class="inlinecode"><span class="id" title="tactic">rewrite</span></span>.  What are the situations where both can usefully be
    applied? 
</div>
<div class="code">

<br/>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
<font size=-2>&#9744;</font>
</div>


<div class="doc">
<a id="lab143"></a><h1 class="section">The <span class="inlinecode"><span class="id" title="tactic">apply</span></span> <span class="inlinecode"><span class="id" title="keyword">with</span></span> Tactic</h1>

<div class="paragraph"> </div>

 The following silly example uses two rewrites in a row to
    get from <span class="inlinecode">[<span class="id" title="var">a</span>;<span class="id" title="var">b</span>]</span> to <span class="inlinecode">[<span class="id" title="var">e</span>;<span class="id" title="var">f</span>]</span>. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Example</span> <a id="trans_eq_example" class="idref" href="#trans_eq_example"><span class="id" title="definition">trans_eq_example</span></a> : <span class="id" title="keyword">∀</span> (<a id="a:17" class="idref" href="#a:17"><span class="id" title="binder">a</span></a> <a id="b:18" class="idref" href="#b:18"><span class="id" title="binder">b</span></a> <a id="c:19" class="idref" href="#c:19"><span class="id" title="binder">c</span></a> <a id="d:20" class="idref" href="#d:20"><span class="id" title="binder">d</span></a> <a id="e:21" class="idref" href="#e:21"><span class="id" title="binder">e</span></a> <a id="f:22" class="idref" href="#f:22"><span class="id" title="binder">f</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Tactics.html#a:17"><span class="id" title="variable">a</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a><a class="idref" href="Tactics.html#b:18"><span class="id" title="variable">b</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Tactics.html#c:19"><span class="id" title="variable">c</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a><a class="idref" href="Tactics.html#d:20"><span class="id" title="variable">d</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Tactics.html#c:19"><span class="id" title="variable">c</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a><a class="idref" href="Tactics.html#d:20"><span class="id" title="variable">d</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Tactics.html#e:21"><span class="id" title="variable">e</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a><a class="idref" href="Tactics.html#f:22"><span class="id" title="variable">f</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Tactics.html#a:17"><span class="id" title="variable">a</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a><a class="idref" href="Tactics.html#b:18"><span class="id" title="variable">b</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Tactics.html#e:21"><span class="id" title="variable">e</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a><a class="idref" href="Tactics.html#f:22"><span class="id" title="variable">f</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">a</span> <span class="id" title="var">b</span> <span class="id" title="var">c</span> <span class="id" title="var">d</span> <span class="id" title="var">e</span> <span class="id" title="var">f</span> <span class="id" title="var">eq<sub>1</sub></span> <span class="id" title="var">eq<sub>2</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">rewrite</span> → <span class="id" title="var">eq<sub>1</sub></span>. <span class="id" title="tactic">rewrite</span> → <span class="id" title="var">eq<sub>2</sub></span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
Since this is a common pattern, we might like to pull it out as a
    lemma that records, once and for all, the fact that equality is
    transitive. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Theorem</span> <a id="trans_eq" class="idref" href="#trans_eq"><span class="id" title="lemma">trans_eq</span></a> : <span class="id" title="keyword">∀</span> (<a id="X:23" class="idref" href="#X:23"><span class="id" title="binder">X</span></a>:<span class="id" title="keyword">Type</span>) (<a id="n:24" class="idref" href="#n:24"><span class="id" title="binder">n</span></a> <a id="m:25" class="idref" href="#m:25"><span class="id" title="binder">m</span></a> <a id="o:26" class="idref" href="#o:26"><span class="id" title="binder">o</span></a> : <a class="idref" href="Tactics.html#X:23"><span class="id" title="variable">X</span></a>),<br/>
&nbsp;&nbsp;<a class="idref" href="Tactics.html#n:24"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Tactics.html#m:25"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Tactics.html#m:25"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Tactics.html#o:26"><span class="id" title="variable">o</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Tactics.html#n:24"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Tactics.html#o:26"><span class="id" title="variable">o</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">X</span> <span class="id" title="var">n</span> <span class="id" title="var">m</span> <span class="id" title="var">o</span> <span class="id" title="var">eq<sub>1</sub></span> <span class="id" title="var">eq<sub>2</sub></span>. <span class="id" title="tactic">rewrite</span> → <span class="id" title="var">eq<sub>1</sub></span>. <span class="id" title="tactic">rewrite</span> → <span class="id" title="var">eq<sub>2</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
Now, we should be able to use <span class="inlinecode"><span class="id" title="var">trans_eq</span></span> to prove the above
    example.  However, to do this we need a slight refinement of the
    <span class="inlinecode"><span class="id" title="tactic">apply</span></span> tactic. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Example</span> <a id="trans_eq_example'" class="idref" href="#trans_eq_example'"><span class="id" title="definition">trans_eq_example'</span></a> : <span class="id" title="keyword">∀</span> (<a id="a:27" class="idref" href="#a:27"><span class="id" title="binder">a</span></a> <a id="b:28" class="idref" href="#b:28"><span class="id" title="binder">b</span></a> <a id="c:29" class="idref" href="#c:29"><span class="id" title="binder">c</span></a> <a id="d:30" class="idref" href="#d:30"><span class="id" title="binder">d</span></a> <a id="e:31" class="idref" href="#e:31"><span class="id" title="binder">e</span></a> <a id="f:32" class="idref" href="#f:32"><span class="id" title="binder">f</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Tactics.html#a:27"><span class="id" title="variable">a</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a><a class="idref" href="Tactics.html#b:28"><span class="id" title="variable">b</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Tactics.html#c:29"><span class="id" title="variable">c</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a><a class="idref" href="Tactics.html#d:30"><span class="id" title="variable">d</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Tactics.html#c:29"><span class="id" title="variable">c</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a><a class="idref" href="Tactics.html#d:30"><span class="id" title="variable">d</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Tactics.html#e:31"><span class="id" title="variable">e</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a><a class="idref" href="Tactics.html#f:32"><span class="id" title="variable">f</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Tactics.html#a:27"><span class="id" title="variable">a</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a><a class="idref" href="Tactics.html#b:28"><span class="id" title="variable">b</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Tactics.html#e:31"><span class="id" title="variable">e</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a><a class="idref" href="Tactics.html#f:32"><span class="id" title="variable">f</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">a</span> <span class="id" title="var">b</span> <span class="id" title="var">c</span> <span class="id" title="var">d</span> <span class="id" title="var">e</span> <span class="id" title="var">f</span> <span class="id" title="var">eq<sub>1</sub></span> <span class="id" title="var">eq<sub>2</sub></span>.<br/>
</div>

<div class="doc">
If we simply tell Coq <span class="inlinecode"><span class="id" title="tactic">apply</span></span> <span class="inlinecode"><span class="id" title="var">trans_eq</span></span> at this point, it can
    tell (by matching the goal against the conclusion of the lemma)
    that it should instantiate <span class="inlinecode"><span class="id" title="var">X</span></span> with <span class="inlinecode">[<span class="id" title="var">nat</span>]</span>, <span class="inlinecode"><span class="id" title="var">n</span></span> with <span class="inlinecode">[<span class="id" title="var">a</span>,<span class="id" title="var">b</span>]</span>, and
    <span class="inlinecode"><span class="id" title="var">o</span></span> with <span class="inlinecode">[<span class="id" title="var">e</span>,<span class="id" title="var">f</span>]</span>.  However, the matching process doesn't determine
    an instantiation for <span class="inlinecode"><span class="id" title="var">m</span></span>: we have to supply one explicitly by
    adding "<span class="inlinecode"><span class="id" title="keyword">with</span></span> <span class="inlinecode">(<span class="id" title="var">m</span>:=[<span class="id" title="var">c</span>,<span class="id" title="var">d</span>])</span>" to the invocation of <span class="inlinecode"><span class="id" title="tactic">apply</span></span>. 
</div>
<div class="code">

<br/>
&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <a class="idref" href="Tactics.html#trans_eq"><span class="id" title="lemma">trans_eq</span></a> <span class="id" title="keyword">with</span> (<span class="id" title="var">m</span>:=<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><span class="id" title="var">c</span><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a><span class="id" title="var">d</span><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a>).<br/>
&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <span class="id" title="var">eq<sub>1</sub></span>. <span class="id" title="tactic">apply</span> <span class="id" title="var">eq<sub>2</sub></span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
(Actually, we usually don't have to include the name <span class="inlinecode"><span class="id" title="var">m</span></span> in
    the <span class="inlinecode"><span class="id" title="keyword">with</span></span> clause; Coq is often smart enough to figure out which
    variable we are instantiating. We could instead write <span class="inlinecode"><span class="id" title="tactic">apply</span></span>
    <span class="inlinecode"><span class="id" title="var">trans_eq</span></span> <span class="inlinecode"><span class="id" title="keyword">with</span></span> <span class="inlinecode">[<span class="id" title="var">c</span>;<span class="id" title="var">d</span>]</span>.) 
<div class="paragraph"> </div>

 Coq also has a tactic <span class="inlinecode"><span class="id" title="tactic">transitivity</span></span> that accomplishes the
    same purpose as applying <span class="inlinecode"><span class="id" title="var">trans_eq</span></span>. The tactic requires us to
    state the instantiation we want, just like <span class="inlinecode"><span class="id" title="tactic">apply</span></span> <span class="inlinecode"><span class="id" title="keyword">with</span></span> does. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Example</span> <a id="trans_eq_example''" class="idref" href="#trans_eq_example''"><span class="id" title="definition">trans_eq_example''</span></a> : <span class="id" title="keyword">∀</span> (<a id="a:33" class="idref" href="#a:33"><span class="id" title="binder">a</span></a> <a id="b:34" class="idref" href="#b:34"><span class="id" title="binder">b</span></a> <a id="c:35" class="idref" href="#c:35"><span class="id" title="binder">c</span></a> <a id="d:36" class="idref" href="#d:36"><span class="id" title="binder">d</span></a> <a id="e:37" class="idref" href="#e:37"><span class="id" title="binder">e</span></a> <a id="f:38" class="idref" href="#f:38"><span class="id" title="binder">f</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Tactics.html#a:33"><span class="id" title="variable">a</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a><a class="idref" href="Tactics.html#b:34"><span class="id" title="variable">b</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Tactics.html#c:35"><span class="id" title="variable">c</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a><a class="idref" href="Tactics.html#d:36"><span class="id" title="variable">d</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Tactics.html#c:35"><span class="id" title="variable">c</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a><a class="idref" href="Tactics.html#d:36"><span class="id" title="variable">d</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Tactics.html#e:37"><span class="id" title="variable">e</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a><a class="idref" href="Tactics.html#f:38"><span class="id" title="variable">f</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Tactics.html#a:33"><span class="id" title="variable">a</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a><a class="idref" href="Tactics.html#b:34"><span class="id" title="variable">b</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Tactics.html#e:37"><span class="id" title="variable">e</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a><a class="idref" href="Tactics.html#f:38"><span class="id" title="variable">f</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">a</span> <span class="id" title="var">b</span> <span class="id" title="var">c</span> <span class="id" title="var">d</span> <span class="id" title="var">e</span> <span class="id" title="var">f</span> <span class="id" title="var">eq<sub>1</sub></span> <span class="id" title="var">eq<sub>2</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">transitivity</span> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><span class="id" title="var">c</span><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a><span class="id" title="var">d</span><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <span class="id" title="var">eq<sub>1</sub></span>. <span class="id" title="tactic">apply</span> <span class="id" title="var">eq<sub>2</sub></span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a id="lab144"></a><h4 class="section">Exercise: 3 stars, standard, optional (trans_eq_exercise)</h4>

</div>
<div class="code">
<span class="id" title="keyword">Example</span> <a id="trans_eq_exercise" class="idref" href="#trans_eq_exercise"><span class="id" title="definition">trans_eq_exercise</span></a> : <span class="id" title="keyword">∀</span> (<a id="n:39" class="idref" href="#n:39"><span class="id" title="binder">n</span></a> <a id="m:40" class="idref" href="#m:40"><span class="id" title="binder">m</span></a> <a id="o:41" class="idref" href="#o:41"><span class="id" title="binder">o</span></a> <a id="p:42" class="idref" href="#p:42"><span class="id" title="binder">p</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Tactics.html#m:40"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="Basics.html#minustwo"><span class="id" title="definition">minustwo</span></a> <a class="idref" href="Tactics.html#o:41"><span class="id" title="variable">o</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="Tactics.html#n:39"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <a class="idref" href="Tactics.html#p:42"><span class="id" title="variable">p</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Tactics.html#m:40"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="Tactics.html#n:39"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <a class="idref" href="Tactics.html#p:42"><span class="id" title="variable">p</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="Basics.html#minustwo"><span class="id" title="definition">minustwo</span></a> <a class="idref" href="Tactics.html#o:41"><span class="id" title="variable">o</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>


<div class="doc">
<a id="lab145"></a><h1 class="section">The <span class="inlinecode"><span class="id" title="tactic">injection</span></span> and <span class="inlinecode"><span class="id" title="tactic">discriminate</span></span> Tactics</h1>

<div class="paragraph"> </div>

 Recall the definition of natural numbers:
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">Inductive</span> <span class="id" title="var">nat</span> : <span class="id" title="keyword">Type</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">O</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">S</span> (<span class="id" title="var">n</span> : <span class="id" title="var">nat</span>).
<div class="paragraph"> </div>

</span>    It is obvious from this definition that every number has one of
    two forms: either it is the constructor <span class="inlinecode"><span class="id" title="var">O</span></span> or it is built by
    applying the constructor <span class="inlinecode"><span class="id" title="var">S</span></span> to another number.  But there is more
    here than meets the eye: implicit in the definition are two more
    facts:

<div class="paragraph"> </div>

<ul class="doclist">
<li> The constructor <span class="inlinecode"><span class="id" title="var">S</span></span> is <i>injective</i>, or <i>one-to-one</i>.  That is,
      if <span class="inlinecode"><span class="id" title="var">S</span></span> <span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">S</span></span> <span class="inlinecode"><span class="id" title="var">m</span></span>, it must be that <span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">m</span></span>.

<div class="paragraph"> </div>


</li>
<li> The constructors <span class="inlinecode"><span class="id" title="var">O</span></span> and <span class="inlinecode"><span class="id" title="var">S</span></span> are <i>disjoint</i>.  That is, <span class="inlinecode"><span class="id" title="var">O</span></span> is not
      equal to <span class="inlinecode"><span class="id" title="var">S</span></span> <span class="inlinecode"><span class="id" title="var">n</span></span> for any <span class="inlinecode"><span class="id" title="var">n</span></span>. 
</li>
</ul>

<div class="paragraph"> </div>

 Similar principles apply to all inductively defined types: all
    constructors are injective, and the values built from distinct
    constructors are never equal.  For lists, the <span class="inlinecode"><span class="id" title="var">cons</span></span> constructor
    is injective and <span class="inlinecode"><span class="id" title="var">nil</span></span> is different from every non-empty list.
    For booleans, <span class="inlinecode"><span class="id" title="var">true</span></span> and <span class="inlinecode"><span class="id" title="var">false</span></span> are different.  (Since <span class="inlinecode"><span class="id" title="var">true</span></span> and
    <span class="inlinecode"><span class="id" title="var">false</span></span> take no arguments, their injectivity is neither here
    nor there.)  And so on. 
<div class="paragraph"> </div>

 For example, we can prove the injectivity of <span class="inlinecode"><span class="id" title="var">S</span></span> by using the
    <span class="inlinecode"><span class="id" title="var">pred</span></span> function defined in <span class="inlinecode"><span class="id" title="var">Basics.v</span></span>. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Theorem</span> <a id="S_injective" class="idref" href="#S_injective"><span class="id" title="lemma">S_injective</span></a> : <span class="id" title="keyword">∀</span> (<a id="n:43" class="idref" href="#n:43"><span class="id" title="binder">n</span></a> <a id="m:44" class="idref" href="#m:44"><span class="id" title="binder">m</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>),<br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <a class="idref" href="Tactics.html#n:43"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <a class="idref" href="Tactics.html#m:44"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="Tactics.html#n:43"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Tactics.html#m:44"><span class="id" title="variable">m</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">n</span> <span class="id" title="var">m</span> <span class="id" title="var">H<sub>1</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">assert</span> (<span class="id" title="var">H<sub>2</sub></span>: <span class="id" title="var">n</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#pred"><span class="id" title="abbreviation">pred</span></a> (<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <span class="id" title="var">n</span>)). { <span class="id" title="tactic">reflexivity</span>. }<br/>
&nbsp;&nbsp;<span class="id" title="tactic">rewrite</span> <span class="id" title="var">H<sub>2</sub></span>. <span class="id" title="tactic">rewrite</span> <span class="id" title="var">H<sub>1</sub></span>. <span class="id" title="tactic">reflexivity</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
This technique can be generalized to any constructor by
    writing the equivalent of <span class="inlinecode"><span class="id" title="var">pred</span></span> -- i.e., writing a function that
    "undoes" one application of the constructor. As a more convenient
    alternative, Coq provides a tactic called <span class="inlinecode"><span class="id" title="tactic">injection</span></span> that allows
    us to exploit the injectivity of any constructor.  Here is an
    alternate proof of the above theorem using <span class="inlinecode"><span class="id" title="tactic">injection</span></span>: 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Theorem</span> <a id="S_injective'" class="idref" href="#S_injective'"><span class="id" title="lemma">S_injective'</span></a> : <span class="id" title="keyword">∀</span> (<a id="n:45" class="idref" href="#n:45"><span class="id" title="binder">n</span></a> <a id="m:46" class="idref" href="#m:46"><span class="id" title="binder">m</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>),<br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <a class="idref" href="Tactics.html#n:45"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <a class="idref" href="Tactics.html#m:46"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="Tactics.html#n:45"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Tactics.html#m:46"><span class="id" title="variable">m</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">n</span> <span class="id" title="var">m</span> <span class="id" title="var">H</span>.<br/>
</div>

<div class="doc">
By writing <span class="inlinecode"><span class="id" title="tactic">injection</span></span> <span class="inlinecode"><span class="id" title="var">H</span></span> <span class="inlinecode"><span class="id" title="keyword">as</span></span> <span class="inlinecode"><span class="id" title="var">Hmn</span></span> at this point, we are asking Coq
    to generate all equations that it can infer from <span class="inlinecode"><span class="id" title="var">H</span></span> using the
    injectivity of constructors (in the present example, the equation
    <span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">m</span></span>). Each such equation is added as a hypothesis (with the
    name <span class="inlinecode"><span class="id" title="var">Hmn</span></span> in this case) into the context. 
</div>
<div class="code">

<br/>
&nbsp;&nbsp;<span class="id" title="tactic">injection</span> <span class="id" title="var">H</span> <span class="id" title="keyword">as</span> <span class="id" title="var">Hnm</span>. <span class="id" title="tactic">apply</span> <span class="id" title="var">Hnm</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
Here's a more interesting example that shows how <span class="inlinecode"><span class="id" title="tactic">injection</span></span> can
    derive multiple equations at once. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Theorem</span> <a id="injection_ex<sub>1</sub>" class="idref" href="#injection_ex<sub>1</sub>"><span class="id" title="lemma">injection_ex<sub>1</sub></span></a> : <span class="id" title="keyword">∀</span> (<a id="n:47" class="idref" href="#n:47"><span class="id" title="binder">n</span></a> <a id="m:48" class="idref" href="#m:48"><span class="id" title="binder">m</span></a> <a id="o:49" class="idref" href="#o:49"><span class="id" title="binder">o</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>),<br/>
&nbsp;&nbsp;<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Tactics.html#n:47"><span class="id" title="variable">n</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a> <a class="idref" href="Tactics.html#m:48"><span class="id" title="variable">m</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Tactics.html#o:49"><span class="id" title="variable">o</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a> <a class="idref" href="Tactics.html#o:49"><span class="id" title="variable">o</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Tactics.html#n:47"><span class="id" title="variable">n</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Tactics.html#m:48"><span class="id" title="variable">m</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">n</span> <span class="id" title="var">m</span> <span class="id" title="var">o</span> <span class="id" title="var">H</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;WORKED&nbsp;IN&nbsp;CLASS&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" title="tactic">injection</span> <span class="id" title="var">H</span> <span class="id" title="keyword">as</span> <span class="id" title="var">H<sub>1</sub></span> <span class="id" title="var">H<sub>2</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">rewrite</span> <span class="id" title="var">H<sub>1</sub></span>. <span class="id" title="tactic">rewrite</span> <span class="id" title="var">H<sub>2</sub></span>. <span class="id" title="tactic">reflexivity</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
Alternatively, if you just say <span class="inlinecode"><span class="id" title="tactic">injection</span></span> <span class="inlinecode"><span class="id" title="var">H</span></span> with no <span class="inlinecode"><span class="id" title="keyword">as</span></span> clause,
    then all the equations will be turned into hypotheses at the
    beginning of the goal. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Theorem</span> <a id="injection_ex<sub>2</sub>" class="idref" href="#injection_ex<sub>2</sub>"><span class="id" title="lemma">injection_ex<sub>2</sub></span></a> : <span class="id" title="keyword">∀</span> (<a id="n:50" class="idref" href="#n:50"><span class="id" title="binder">n</span></a> <a id="m:51" class="idref" href="#m:51"><span class="id" title="binder">m</span></a> <a id="o:52" class="idref" href="#o:52"><span class="id" title="binder">o</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>),<br/>
&nbsp;&nbsp;<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Tactics.html#n:50"><span class="id" title="variable">n</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a> <a class="idref" href="Tactics.html#m:51"><span class="id" title="variable">m</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Tactics.html#o:52"><span class="id" title="variable">o</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a> <a class="idref" href="Tactics.html#o:52"><span class="id" title="variable">o</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Tactics.html#n:50"><span class="id" title="variable">n</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Tactics.html#m:51"><span class="id" title="variable">m</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">n</span> <span class="id" title="var">m</span> <span class="id" title="var">o</span> <span class="id" title="var">H</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">injection</span> <span class="id" title="var">H</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;WORKED&nbsp;IN&nbsp;CLASS&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">H<sub>1</sub></span> <span class="id" title="var">H<sub>2</sub></span>. <span class="id" title="tactic">rewrite</span> <span class="id" title="var">H<sub>1</sub></span>. <span class="id" title="tactic">rewrite</span> <span class="id" title="var">H<sub>2</sub></span>. <span class="id" title="tactic">reflexivity</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a id="lab146"></a><h4 class="section">Exercise: 3 stars, standard (injection_ex<sub>3</sub>)</h4>

</div>
<div class="code">
<span class="id" title="keyword">Example</span> <a id="injection_ex<sub>3</sub>" class="idref" href="#injection_ex<sub>3</sub>"><span class="id" title="definition">injection_ex<sub>3</sub></span></a> : <span class="id" title="keyword">∀</span> (<a id="X:53" class="idref" href="#X:53"><span class="id" title="binder">X</span></a> : <span class="id" title="keyword">Type</span>) (<a id="x:54" class="idref" href="#x:54"><span class="id" title="binder">x</span></a> <a id="y:55" class="idref" href="#y:55"><span class="id" title="binder">y</span></a> <a id="z:56" class="idref" href="#z:56"><span class="id" title="binder">z</span></a> : <a class="idref" href="Tactics.html#X:53"><span class="id" title="variable">X</span></a>) (<a id="l:57" class="idref" href="#l:57"><span class="id" title="binder">l</span></a> <a id="j:58" class="idref" href="#j:58"><span class="id" title="binder">j</span></a> : <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Tactics.html#X:53"><span class="id" title="variable">X</span></a>),<br/>
&nbsp;&nbsp;<a class="idref" href="Tactics.html#x:54"><span class="id" title="variable">x</span></a> <a class="idref" href="Poly.html#:::x_'::'_x"><span class="id" title="notation">::</span></a> <a class="idref" href="Tactics.html#y:55"><span class="id" title="variable">y</span></a> <a class="idref" href="Poly.html#:::x_'::'_x"><span class="id" title="notation">::</span></a> <a class="idref" href="Tactics.html#l:57"><span class="id" title="variable">l</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Tactics.html#z:56"><span class="id" title="variable">z</span></a> <a class="idref" href="Poly.html#:::x_'::'_x"><span class="id" title="notation">::</span></a> <a class="idref" href="Tactics.html#j:58"><span class="id" title="variable">j</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="Tactics.html#j:58"><span class="id" title="variable">j</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Tactics.html#z:56"><span class="id" title="variable">z</span></a> <a class="idref" href="Poly.html#:::x_'::'_x"><span class="id" title="notation">::</span></a> <a class="idref" href="Tactics.html#l:57"><span class="id" title="variable">l</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="Tactics.html#x:54"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Tactics.html#y:55"><span class="id" title="variable">y</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

 So much for injectivity of constructors.  What about disjointness?

<div class="paragraph"> </div>

    The principle of disjointness says that two terms beginning with
    different constructors (like <span class="inlinecode"><span class="id" title="var">O</span></span> and <span class="inlinecode"><span class="id" title="var">S</span></span>, or <span class="inlinecode"><span class="id" title="var">true</span></span> and <span class="inlinecode"><span class="id" title="var">false</span></span>)
    can never be equal.  This means that, any time we find ourselves
    in a context where we've <i>assumed</i> that two such terms are equal,
    we are justified in concluding anything we want, since the
    assumption is nonsensical. 
<div class="paragraph"> </div>

 The <span class="inlinecode"><span class="id" title="tactic">discriminate</span></span> tactic embodies this principle: It is used on a
    hypothesis involving an equality between different
    constructors (e.g., <span class="inlinecode"><span class="id" title="var">S</span></span> <span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">O</span></span>), and it solves the current goal
    immediately.  Here is an example: 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Theorem</span> <a id="eqb_0_l" class="idref" href="#eqb_0_l"><span class="id" title="lemma">eqb_0_l</span></a> : <span class="id" title="keyword">∀</span> <a id="n:59" class="idref" href="#n:59"><span class="id" title="binder">n</span></a>,<br/>
&nbsp;&nbsp;&nbsp;0 <a class="idref" href="Basics.html#ad2ec4e405f68c46c0a176e3e94ae2e<sub>3</sub>"><span class="id" title="notation">=?</span></a> <a class="idref" href="Tactics.html#n:59"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Tactics.html#n:59"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 0.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">n</span>.<br/>
</div>

<div class="doc">
We can proceed by case analysis on <span class="inlinecode"><span class="id" title="var">n</span></span>. The first case is
    trivial. 
</div>
<div class="code">

<br/>
&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> <span class="id" title="var">n</span> <span class="id" title="keyword">as</span> [| <span class="id" title="var">n'</span>] <span class="id" title="var">eqn</span>:<span class="id" title="var">E</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;n&nbsp;=&nbsp;0&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">H</span>. <span class="id" title="tactic">reflexivity</span>.<br/>
</div>

<div class="doc">
However, the second one doesn't look so simple: assuming <span class="inlinecode">0</span>
    <span class="inlinecode">=?</span> <span class="inlinecode">(<span class="id" title="var">S</span></span> <span class="inlinecode"><span class="id" title="var">n'</span>)</span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">true</span></span>, we must show <span class="inlinecode"><span class="id" title="var">S</span></span> <span class="inlinecode"><span class="id" title="var">n'</span></span> <span class="inlinecode">=</span> <span class="inlinecode">0</span>!  The way forward is to
    observe that the assumption itself is nonsensical: 
</div>
<div class="code">

<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;n&nbsp;=&nbsp;S&nbsp;n'&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">simpl</span>.<br/>
</div>

<div class="doc">
If we use <span class="inlinecode"><span class="id" title="tactic">discriminate</span></span> on this hypothesis, Coq confirms
    that the subgoal we are working on is impossible and removes it
    from further consideration. 
</div>
<div class="code">

<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">H</span>. <span class="id" title="tactic">discriminate</span> <span class="id" title="var">H</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
This is an instance of a logical principle known as the <i>principle
    of explosion</i>, which asserts that a contradictory hypothesis
    entails anything (even false things!). 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Theorem</span> <a id="discriminate_ex<sub>1</sub>" class="idref" href="#discriminate_ex<sub>1</sub>"><span class="id" title="lemma">discriminate_ex<sub>1</sub></span></a> : <span class="id" title="keyword">∀</span> (<a id="n:60" class="idref" href="#n:60"><span class="id" title="binder">n</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>),<br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <a class="idref" href="Tactics.html#n:60"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#O"><span class="id" title="constructor">O</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;2 <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> 2 <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 5.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">n</span> <span class="id" title="var">contra</span>. <span class="id" title="tactic">discriminate</span> <span class="id" title="var">contra</span>. <span class="id" title="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Theorem</span> <a id="discriminate_ex<sub>2</sub>" class="idref" href="#discriminate_ex<sub>2</sub>"><span class="id" title="lemma">discriminate_ex<sub>2</sub></span></a> : <span class="id" title="keyword">∀</span> (<a id="n:61" class="idref" href="#n:61"><span class="id" title="binder">n</span></a> <a id="m:62" class="idref" href="#m:62"><span class="id" title="binder">m</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>),<br/>
&nbsp;&nbsp;<a class="idref" href="Basics.html#false"><span class="id" title="constructor">false</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Tactics.html#n:61"><span class="id" title="variable">n</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Tactics.html#m:62"><span class="id" title="variable">m</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">n</span> <span class="id" title="var">m</span> <span class="id" title="var">contra</span>. <span class="id" title="tactic">discriminate</span> <span class="id" title="var">contra</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
If you find the principle of explosion confusing, remember
    that these proofs are <i>not</i> showing that the conclusion of the
    statement holds.  Rather, they are showing that, <i>if</i> the
    nonsensical situation described by the premise did somehow arise,
    <i>then</i> the nonsensical conclusion would also follow, because we'd
    be living in an inconsistent universe where every statement is
    true.  We'll explore the principle of explosion in more detail in
    the next chapter. 
<div class="paragraph"> </div>

<a id="lab147"></a><h4 class="section">Exercise: 1 star, standard (discriminate_ex<sub>3</sub>)</h4>

</div>
<div class="code">
<span class="id" title="keyword">Example</span> <a id="discriminate_ex<sub>3</sub>" class="idref" href="#discriminate_ex<sub>3</sub>"><span class="id" title="definition">discriminate_ex<sub>3</sub></span></a> :<br/>
&nbsp;&nbsp;<span class="id" title="keyword">∀</span> (<a id="X:63" class="idref" href="#X:63"><span class="id" title="binder">X</span></a> : <span class="id" title="keyword">Type</span>) (<a id="x:64" class="idref" href="#x:64"><span class="id" title="binder">x</span></a> <a id="y:65" class="idref" href="#y:65"><span class="id" title="binder">y</span></a> <a id="z:66" class="idref" href="#z:66"><span class="id" title="binder">z</span></a> : <a class="idref" href="Tactics.html#X:63"><span class="id" title="variable">X</span></a>) (<a id="l:67" class="idref" href="#l:67"><span class="id" title="binder">l</span></a> <a id="j:68" class="idref" href="#j:68"><span class="id" title="binder">j</span></a> : <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Tactics.html#X:63"><span class="id" title="variable">X</span></a>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Tactics.html#x:64"><span class="id" title="variable">x</span></a> <a class="idref" href="Poly.html#:::x_'::'_x"><span class="id" title="notation">::</span></a> <a class="idref" href="Tactics.html#y:65"><span class="id" title="variable">y</span></a> <a class="idref" href="Poly.html#:::x_'::'_x"><span class="id" title="notation">::</span></a> <a class="idref" href="Tactics.html#l:67"><span class="id" title="variable">l</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#2c60282cbb04e070c60ae01e76f3865a"><span class="id" title="notation">[]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Tactics.html#x:64"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Tactics.html#z:66"><span class="id" title="variable">z</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

 The injectivity of constructors allows us to reason that
    <span class="inlinecode"><span class="id" title="keyword">∀</span></span> <span class="inlinecode">(<span class="id" title="var">n</span></span> <span class="inlinecode"><span class="id" title="var">m</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" title="var">nat</span>),</span> <span class="inlinecode"><span class="id" title="var">S</span></span> <span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">S</span></span> <span class="inlinecode"><span class="id" title="var">m</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">m</span></span>.  The converse of this
    implication is an instance of a more general fact about both
    constructors and functions, which we will find convenient in a few
    places below: 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Theorem</span> <a id="f_equal" class="idref" href="#f_equal"><span class="id" title="lemma">f_equal</span></a> : <span class="id" title="keyword">∀</span> (<a id="A:69" class="idref" href="#A:69"><span class="id" title="binder">A</span></a> <a id="B:70" class="idref" href="#B:70"><span class="id" title="binder">B</span></a> : <span class="id" title="keyword">Type</span>) (<a id="f:71" class="idref" href="#f:71"><span class="id" title="binder">f</span></a>: <a class="idref" href="Tactics.html#A:69"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Tactics.html#B:70"><span class="id" title="variable">B</span></a>) (<a id="x:72" class="idref" href="#x:72"><span class="id" title="binder">x</span></a> <a id="y:73" class="idref" href="#y:73"><span class="id" title="binder">y</span></a>: <a class="idref" href="Tactics.html#A:69"><span class="id" title="variable">A</span></a>),<br/>
&nbsp;&nbsp;<a class="idref" href="Tactics.html#x:72"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Tactics.html#y:73"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Tactics.html#f:71"><span class="id" title="variable">f</span></a> <a class="idref" href="Tactics.html#x:72"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Tactics.html#f:71"><span class="id" title="variable">f</span></a> <a class="idref" href="Tactics.html#y:73"><span class="id" title="variable">y</span></a>.<br/>
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">intros</span> <span class="id" title="var">A</span> <span class="id" title="var">B</span> <span class="id" title="var">f</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">eq</span>. <span class="id" title="tactic">rewrite</span> <span class="id" title="var">eq</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Theorem</span> <a id="eq_implies_succ_equal" class="idref" href="#eq_implies_succ_equal"><span class="id" title="lemma">eq_implies_succ_equal</span></a> : <span class="id" title="keyword">∀</span> (<a id="n:74" class="idref" href="#n:74"><span class="id" title="binder">n</span></a> <a id="m:75" class="idref" href="#m:75"><span class="id" title="binder">m</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Tactics.html#n:74"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Tactics.html#m:75"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <a class="idref" href="Tactics.html#n:74"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <a class="idref" href="Tactics.html#m:75"><span class="id" title="variable">m</span></a>.<br/>
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">intros</span> <span class="id" title="var">n</span> <span class="id" title="var">m</span> <span class="id" title="var">H</span>. <span class="id" title="tactic">apply</span> <a class="idref" href="Tactics.html#f_equal"><span class="id" title="lemma">f_equal</span></a>. <span class="id" title="tactic">apply</span> <span class="id" title="var">H</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
There is also a tactic named `f_equal` that can prove such
    theorems.  Given a goal of the form <span class="inlinecode"><span class="id" title="var">f</span></span> <span class="inlinecode"><span class="id" title="var">a<sub>1</sub></span></span> <span class="inlinecode">...</span> <span class="inlinecode"><span class="id" title="var">an</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">g</span></span> <span class="inlinecode"><span class="id" title="var">b<sub>1</sub></span></span> <span class="inlinecode">...</span> <span class="inlinecode"><span class="id" title="var">bn</span></span>,
    the tactic <span class="inlinecode"><span class="id" title="tactic">f_equal</span></span> will produce subgoals of the form <span class="inlinecode"><span class="id" title="var">f</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">g</span></span>,
    <span class="inlinecode"><span class="id" title="var">a<sub>1</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">b<sub>1</sub></span></span>, ..., <span class="inlinecode"><span class="id" title="var">an</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">bn</span></span>. At the same time, any of these subgoals
    that are simple enough (e.g., immediately provable by
    <span class="inlinecode"><span class="id" title="tactic">reflexivity</span></span>) will be automatically discharged by <span class="inlinecode"><span class="id" title="tactic">f_equal</span></span>. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Theorem</span> <a id="eq_implies_succ_equal'" class="idref" href="#eq_implies_succ_equal'"><span class="id" title="lemma">eq_implies_succ_equal'</span></a> : <span class="id" title="keyword">∀</span> (<a id="n:76" class="idref" href="#n:76"><span class="id" title="binder">n</span></a> <a id="m:77" class="idref" href="#m:77"><span class="id" title="binder">m</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Tactics.html#n:76"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Tactics.html#m:77"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <a class="idref" href="Tactics.html#n:76"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <a class="idref" href="Tactics.html#m:77"><span class="id" title="variable">m</span></a>.<br/>
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">intros</span> <span class="id" title="var">n</span> <span class="id" title="var">m</span> <span class="id" title="var">H</span>. <span class="id" title="tactic">f_equal</span>. <span class="id" title="tactic">apply</span> <span class="id" title="var">H</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a id="lab148"></a><h1 class="section">Using Tactics on Hypotheses</h1>

<div class="paragraph"> </div>

 By default, most tactics work on the goal formula and leave
    the context unchanged.  However, most tactics also have a variant
    that performs a similar operation on a statement in the context.

<div class="paragraph"> </div>

    For example, the tactic "<span class="inlinecode"><span class="id" title="tactic">simpl</span></span> <span class="inlinecode"><span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">H</span></span>" performs simplification on
    the hypothesis <span class="inlinecode"><span class="id" title="var">H</span></span> in the context. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Theorem</span> <a id="S_inj" class="idref" href="#S_inj"><span class="id" title="lemma">S_inj</span></a> : <span class="id" title="keyword">∀</span> (<a id="n:78" class="idref" href="#n:78"><span class="id" title="binder">n</span></a> <a id="m:79" class="idref" href="#m:79"><span class="id" title="binder">m</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) (<a id="b:80" class="idref" href="#b:80"><span class="id" title="binder">b</span></a> : <a class="idref" href="Basics.html#bool"><span class="id" title="inductive">bool</span></a>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Basics.html#ad2ec4e405f68c46c0a176e3e94ae2e<sub>3</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <a class="idref" href="Tactics.html#n:78"><span class="id" title="variable">n</span></a><a class="idref" href="Basics.html#ad2ec4e405f68c46c0a176e3e94ae2e<sub>3</sub>"><span class="id" title="notation">)</span></a> <a class="idref" href="Basics.html#ad2ec4e405f68c46c0a176e3e94ae2e<sub>3</sub>"><span class="id" title="notation">=?</span></a> <a class="idref" href="Basics.html#ad2ec4e405f68c46c0a176e3e94ae2e<sub>3</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <a class="idref" href="Tactics.html#m:79"><span class="id" title="variable">m</span></a><a class="idref" href="Basics.html#ad2ec4e405f68c46c0a176e3e94ae2e<sub>3</sub>"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Tactics.html#b:80"><span class="id" title="variable">b</span></a>  <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Tactics.html#n:78"><span class="id" title="variable">n</span></a> <a class="idref" href="Basics.html#ad2ec4e405f68c46c0a176e3e94ae2e<sub>3</sub>"><span class="id" title="notation">=?</span></a> <a class="idref" href="Tactics.html#m:79"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Tactics.html#b:80"><span class="id" title="variable">b</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">n</span> <span class="id" title="var">m</span> <span class="id" title="var">b</span> <span class="id" title="var">H</span>. <span class="id" title="tactic">simpl</span> <span class="id" title="tactic">in</span> <span class="id" title="var">H</span>. <span class="id" title="tactic">apply</span> <span class="id" title="var">H</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
Similarly, <span class="inlinecode"><span class="id" title="tactic">apply</span></span> <span class="inlinecode"><span class="id" title="var">L</span></span> <span class="inlinecode"><span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">H</span></span> matches some conditional statement
    <span class="inlinecode"><span class="id" title="var">L</span></span> (of the form <span class="inlinecode"><span class="id" title="var">X</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" title="var">Y</span></span>, say) against a hypothesis <span class="inlinecode"><span class="id" title="var">H</span></span> in the
    context.  However, unlike ordinary <span class="inlinecode"><span class="id" title="tactic">apply</span></span> (which rewrites a goal
    matching <span class="inlinecode"><span class="id" title="var">Y</span></span> into a subgoal <span class="inlinecode"><span class="id" title="var">X</span></span>), <span class="inlinecode"><span class="id" title="tactic">apply</span></span> <span class="inlinecode"><span class="id" title="var">L</span></span> <span class="inlinecode"><span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">H</span></span> matches <span class="inlinecode"><span class="id" title="var">H</span></span>
    against <span class="inlinecode"><span class="id" title="var">X</span></span> and, if successful, replaces it with <span class="inlinecode"><span class="id" title="var">Y</span></span>.

<div class="paragraph"> </div>

    In other words, <span class="inlinecode"><span class="id" title="tactic">apply</span></span> <span class="inlinecode"><span class="id" title="var">L</span></span> <span class="inlinecode"><span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">H</span></span> gives us a form of "forward
    reasoning": from <span class="inlinecode"><span class="id" title="var">X</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" title="var">Y</span></span> and a hypothesis matching <span class="inlinecode"><span class="id" title="var">X</span></span>, it
    produces a hypothesis matching <span class="inlinecode"><span class="id" title="var">Y</span></span>.  By contrast, <span class="inlinecode"><span class="id" title="tactic">apply</span></span> <span class="inlinecode"><span class="id" title="var">L</span></span> is
    "backward reasoning": it says that if we know <span class="inlinecode"><span class="id" title="var">X</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" title="var">Y</span></span> and we
    are trying to prove <span class="inlinecode"><span class="id" title="var">Y</span></span>, it suffices to prove <span class="inlinecode"><span class="id" title="var">X</span></span>.

<div class="paragraph"> </div>

    Here is a variant of a proof from above, using forward reasoning
    throughout instead of backward reasoning. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Theorem</span> <a id="silly3'" class="idref" href="#silly3'"><span class="id" title="lemma">silly3'</span></a> : <span class="id" title="keyword">∀</span> (<a id="n:81" class="idref" href="#n:81"><span class="id" title="binder">n</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>),<br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">(</span></a><a class="idref" href="Tactics.html#n:81"><span class="id" title="variable">n</span></a> <a class="idref" href="Basics.html#ad2ec4e405f68c46c0a176e3e94ae2e<sub>3</sub>"><span class="id" title="notation">=?</span></a> 5 <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Basics.html#ad2ec4e405f68c46c0a176e3e94ae2e<sub>3</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> (<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <a class="idref" href="Tactics.html#n:81"><span class="id" title="variable">n</span></a>)<a class="idref" href="Basics.html#ad2ec4e405f68c46c0a176e3e94ae2e<sub>3</sub>"><span class="id" title="notation">)</span></a> <a class="idref" href="Basics.html#ad2ec4e405f68c46c0a176e3e94ae2e<sub>3</sub>"><span class="id" title="notation">=?</span></a> 7 <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="Tactics.html#n:81"><span class="id" title="variable">n</span></a> <a class="idref" href="Basics.html#ad2ec4e405f68c46c0a176e3e94ae2e<sub>3</sub>"><span class="id" title="notation">=?</span></a> 5<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a>  <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="Basics.html#ad2ec4e405f68c46c0a176e3e94ae2e<sub>3</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> (<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <a class="idref" href="Tactics.html#n:81"><span class="id" title="variable">n</span></a>)<a class="idref" href="Basics.html#ad2ec4e405f68c46c0a176e3e94ae2e<sub>3</sub>"><span class="id" title="notation">)</span></a> <a class="idref" href="Basics.html#ad2ec4e405f68c46c0a176e3e94ae2e<sub>3</sub>"><span class="id" title="notation">=?</span></a> 7<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">n</span> <span class="id" title="var">eq</span> <span class="id" title="var">H</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">symmetry</span> <span class="id" title="tactic">in</span> <span class="id" title="var">H</span>. <span class="id" title="tactic">apply</span> <span class="id" title="var">eq</span> <span class="id" title="tactic">in</span> <span class="id" title="var">H</span>. <span class="id" title="tactic">symmetry</span> <span class="id" title="tactic">in</span> <span class="id" title="var">H</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <span class="id" title="var">H</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
Forward reasoning starts from what is <i>given</i> (premises,
    previously proven theorems) and iteratively draws conclusions from
    them until the goal is reached.  Backward reasoning starts from
    the <i>goal</i> and iteratively reasons about what would imply the
    goal, until premises or previously proven theorems are reached.

<div class="paragraph"> </div>

    The informal proofs that you've seen in math or computer science
    classes probably tended to use forward reasoning.  In general,
    idiomatic use of Coq favors backward reasoning, but in some
    situations the forward style can be easier to think about. 
</div>

<div class="doc">
<a id="lab149"></a><h1 class="section">Varying the Induction Hypothesis</h1>

<div class="paragraph"> </div>

 Sometimes it is important to control the exact form of the
    induction hypothesis when carrying out inductive proofs in Coq.
    In particular, we sometimes need to be careful about which of the
    assumptions we move (using <span class="inlinecode"><span class="id" title="tactic">intros</span></span>) from the goal to the context
    before invoking the <span class="inlinecode"><span class="id" title="tactic">induction</span></span> tactic.  For example, suppose
    we want to show that <span class="inlinecode"><span class="id" title="var">double</span></span> is injective -- i.e., that it maps
    different arguments to different results:
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">Theorem</span> <span class="id" title="var">double_injective</span>: <span class="id" title="keyword">∀</span> <span class="id" title="var">n</span> <span class="id" title="var">m</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">double</span> <span class="id" title="var">n</span> = <span class="id" title="var">double</span> <span class="id" title="var">m</span> → <span class="id" title="var">n</span> = <span class="id" title="var">m</span>.
<div class="paragraph"> </div>

</span>    The way we start this proof is a bit delicate: if we begin it with
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">n</span>. <span class="id" title="tactic">induction</span> <span class="id" title="var">n</span>.
<div class="paragraph"> </div>

</span>    all is well.  But if we begin it with
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">n</span> <span class="id" title="var">m</span>. <span class="id" title="tactic">induction</span> <span class="id" title="var">n</span>.
<div class="paragraph"> </div>

</span>    we get stuck in the middle of the inductive case... 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Theorem</span> <a id="double_injective_FAILED" class="idref" href="#double_injective_FAILED"><span class="id" title="lemma">double_injective_FAILED</span></a> : <span class="id" title="keyword">∀</span> <a id="n:82" class="idref" href="#n:82"><span class="id" title="binder">n</span></a> <a id="m:83" class="idref" href="#m:83"><span class="id" title="binder">m</span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Induction.html#double"><span class="id" title="definition">double</span></a> <a class="idref" href="Tactics.html#n:82"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Induction.html#double"><span class="id" title="definition">double</span></a> <a class="idref" href="Tactics.html#m:83"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Tactics.html#n:82"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Tactics.html#m:83"><span class="id" title="variable">m</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">n</span> <span class="id" title="var">m</span>. <span class="id" title="tactic">induction</span> <span class="id" title="var">n</span> <span class="id" title="keyword">as</span> [| <span class="id" title="var">n'</span> <span class="id" title="var">IHn'</span>].<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;n&nbsp;=&nbsp;O&nbsp;*)</span> <span class="id" title="tactic">simpl</span>. <span class="id" title="tactic">intros</span> <span class="id" title="var">eq</span>. <span class="id" title="tactic">destruct</span> <span class="id" title="var">m</span> <span class="id" title="keyword">as</span> [| <span class="id" title="var">m'</span>] <span class="id" title="var">eqn</span>:<span class="id" title="var">E</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;m&nbsp;=&nbsp;O&nbsp;*)</span> <span class="id" title="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;m&nbsp;=&nbsp;S&nbsp;m'&nbsp;*)</span> <span class="id" title="tactic">discriminate</span> <span class="id" title="var">eq</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;n&nbsp;=&nbsp;S&nbsp;n'&nbsp;*)</span> <span class="id" title="tactic">intros</span> <span class="id" title="var">eq</span>. <span class="id" title="tactic">destruct</span> <span class="id" title="var">m</span> <span class="id" title="keyword">as</span> [| <span class="id" title="var">m'</span>] <span class="id" title="var">eqn</span>:<span class="id" title="var">E</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;m&nbsp;=&nbsp;O&nbsp;*)</span> <span class="id" title="tactic">discriminate</span> <span class="id" title="var">eq</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;m&nbsp;=&nbsp;S&nbsp;m'&nbsp;*)</span> <span class="id" title="tactic">apply</span> <a class="idref" href="Tactics.html#f_equal"><span class="id" title="lemma">f_equal</span></a>.<br/>
</div>

<div class="doc">
At this point, the induction hypothesis (<span class="inlinecode"><span class="id" title="var">IHn'</span></span>) does <i>not</i> give us
    <span class="inlinecode"><span class="id" title="var">n'</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">m'</span></span> -- there is an extra <span class="inlinecode"><span class="id" title="var">S</span></span> in the way -- so the goal is
    not provable. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Abort</span>.<br/>
</div>

<div class="doc">
What went wrong? 
<div class="paragraph"> </div>

 The problem is that, at the point we invoke the induction
    hypothesis, we have already introduced <span class="inlinecode"><span class="id" title="var">m</span></span> into the context --
    intuitively, we have told Coq, "Let's consider some particular <span class="inlinecode"><span class="id" title="var">n</span></span>
    and <span class="inlinecode"><span class="id" title="var">m</span></span>..." and we now have to prove that, if <span class="inlinecode"><span class="id" title="var">double</span></span> <span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">double</span></span>
    <span class="inlinecode"><span class="id" title="var">m</span></span> for <i>those particular</i> <span class="inlinecode"><span class="id" title="var">n</span></span> and <span class="inlinecode"><span class="id" title="var">m</span></span>, then <span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">m</span></span>.

<div class="paragraph"> </div>

    The next tactic, <span class="inlinecode"><span class="id" title="tactic">induction</span></span> <span class="inlinecode"><span class="id" title="var">n</span></span> says to Coq: We are going to show
    the goal by induction on <span class="inlinecode"><span class="id" title="var">n</span></span>.  That is, we are going to prove, for
    <i>all</i> <span class="inlinecode"><span class="id" title="var">n</span></span>, that the proposition

<div class="paragraph"> </div>

<ul class="doclist">
<li> <span class="inlinecode"><span class="id" title="var">P</span></span> <span class="inlinecode"><span class="id" title="var">n</span></span> = "if <span class="inlinecode"><span class="id" title="var">double</span></span> <span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">double</span></span> <span class="inlinecode"><span class="id" title="var">m</span></span>, then <span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">m</span></span>"

</li>
</ul>

<div class="paragraph"> </div>

    holds, by showing

<div class="paragraph"> </div>

<ul class="doclist">
<li> <span class="inlinecode"><span class="id" title="var">P</span></span> <span class="inlinecode"><span class="id" title="var">O</span></span>

<div class="paragraph"> </div>

         (i.e., "if <span class="inlinecode"><span class="id" title="var">double</span></span> <span class="inlinecode"><span class="id" title="var">O</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">double</span></span> <span class="inlinecode"><span class="id" title="var">m</span></span> then <span class="inlinecode"><span class="id" title="var">O</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">m</span></span>") and

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" title="var">P</span></span> <span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" title="var">P</span></span> <span class="inlinecode">(<span class="id" title="var">S</span></span> <span class="inlinecode"><span class="id" title="var">n</span>)</span>

<div class="paragraph"> </div>

        (i.e., "if <span class="inlinecode"><span class="id" title="var">double</span></span> <span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">double</span></span> <span class="inlinecode"><span class="id" title="var">m</span></span> then <span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">m</span></span>" implies "if
        <span class="inlinecode"><span class="id" title="var">double</span></span> <span class="inlinecode">(<span class="id" title="var">S</span></span> <span class="inlinecode"><span class="id" title="var">n</span>)</span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">double</span></span> <span class="inlinecode"><span class="id" title="var">m</span></span> then <span class="inlinecode"><span class="id" title="var">S</span></span> <span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">m</span></span>").

</li>
</ul>

<div class="paragraph"> </div>

    If we look closely at the second statement, it is saying something
    rather strange: that, for a <i>particular</i> <span class="inlinecode"><span class="id" title="var">m</span></span>, if we know

<div class="paragraph"> </div>

<ul class="doclist">
<li> "if <span class="inlinecode"><span class="id" title="var">double</span></span> <span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">double</span></span> <span class="inlinecode"><span class="id" title="var">m</span></span> then <span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">m</span></span>"

</li>
</ul>

<div class="paragraph"> </div>

    then we can prove

<div class="paragraph"> </div>

<ul class="doclist">
<li> "if <span class="inlinecode"><span class="id" title="var">double</span></span> <span class="inlinecode">(<span class="id" title="var">S</span></span> <span class="inlinecode"><span class="id" title="var">n</span>)</span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">double</span></span> <span class="inlinecode"><span class="id" title="var">m</span></span> then <span class="inlinecode"><span class="id" title="var">S</span></span> <span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">m</span></span>".

</li>
</ul>

<div class="paragraph"> </div>

    To see why this is strange, let's think of a particular (arbitrary,
    but fixed) <span class="inlinecode"><span class="id" title="var">m</span></span> -- say, <span class="inlinecode">5</span>.  The statement is then saying that,
    if we know

<div class="paragraph"> </div>

<ul class="doclist">
<li> <span class="inlinecode"><span class="id" title="var">Q</span></span> = "if <span class="inlinecode"><span class="id" title="var">double</span></span> <span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode">10</span> then <span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode">5</span>"

</li>
</ul>

<div class="paragraph"> </div>

    then we can prove

<div class="paragraph"> </div>

<ul class="doclist">
<li> <span class="inlinecode"><span class="id" title="var">R</span></span> = "if <span class="inlinecode"><span class="id" title="var">double</span></span> <span class="inlinecode">(<span class="id" title="var">S</span></span> <span class="inlinecode"><span class="id" title="var">n</span>)</span> <span class="inlinecode">=</span> <span class="inlinecode">10</span> then <span class="inlinecode"><span class="id" title="var">S</span></span> <span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode">5</span>".

</li>
</ul>

<div class="paragraph"> </div>

    But knowing <span class="inlinecode"><span class="id" title="var">Q</span></span> doesn't give us any help at all with proving
    <span class="inlinecode"><span class="id" title="var">R</span></span>!  If we tried to prove <span class="inlinecode"><span class="id" title="var">R</span></span> from <span class="inlinecode"><span class="id" title="var">Q</span></span>, we would start with
    something like "Suppose <span class="inlinecode"><span class="id" title="var">double</span></span> <span class="inlinecode">(<span class="id" title="var">S</span></span> <span class="inlinecode"><span class="id" title="var">n</span>)</span> <span class="inlinecode">=</span> <span class="inlinecode">10</span>..." but then we'd be
    stuck: knowing that <span class="inlinecode"><span class="id" title="var">double</span></span> <span class="inlinecode">(<span class="id" title="var">S</span></span> <span class="inlinecode"><span class="id" title="var">n</span>)</span> is <span class="inlinecode">10</span> tells us nothing
    helpful about whether <span class="inlinecode"><span class="id" title="var">double</span></span> <span class="inlinecode"><span class="id" title="var">n</span></span> is <span class="inlinecode">10</span> (indeed, it strongly
    suggests that <span class="inlinecode"><span class="id" title="var">double</span></span> <span class="inlinecode"><span class="id" title="var">n</span></span> is <i>not</i> <span class="inlinecode">10</span>!!), so <span class="inlinecode"><span class="id" title="var">Q</span></span> is useless. 
<div class="paragraph"> </div>

 Trying to carry out this proof by induction on <span class="inlinecode"><span class="id" title="var">n</span></span> when <span class="inlinecode"><span class="id" title="var">m</span></span> is
    already in the context doesn't work because we are then trying to
    prove a statement involving <i>every</i> <span class="inlinecode"><span class="id" title="var">n</span></span> but just a <i>single</i> <span class="inlinecode"><span class="id" title="var">m</span></span>. 
<div class="paragraph"> </div>

 A successful proof of <span class="inlinecode"><span class="id" title="var">double_injective</span></span> leaves <span class="inlinecode"><span class="id" title="var">m</span></span> in the goal
    statement at the point where the <span class="inlinecode"><span class="id" title="tactic">induction</span></span> tactic is invoked on
    <span class="inlinecode"><span class="id" title="var">n</span></span>: 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Theorem</span> <a id="double_injective" class="idref" href="#double_injective"><span class="id" title="lemma">double_injective</span></a> : <span class="id" title="keyword">∀</span> <a id="n:84" class="idref" href="#n:84"><span class="id" title="binder">n</span></a> <a id="m:85" class="idref" href="#m:85"><span class="id" title="binder">m</span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Induction.html#double"><span class="id" title="definition">double</span></a> <a class="idref" href="Tactics.html#n:84"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Induction.html#double"><span class="id" title="definition">double</span></a> <a class="idref" href="Tactics.html#m:85"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Tactics.html#n:84"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Tactics.html#m:85"><span class="id" title="variable">m</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">n</span>. <span class="id" title="tactic">induction</span> <span class="id" title="var">n</span> <span class="id" title="keyword">as</span> [| <span class="id" title="var">n'</span> <span class="id" title="var">IHn'</span>].<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;n&nbsp;=&nbsp;O&nbsp;*)</span> <span class="id" title="tactic">simpl</span>. <span class="id" title="tactic">intros</span> <span class="id" title="var">m</span> <span class="id" title="var">eq</span>. <span class="id" title="tactic">destruct</span> <span class="id" title="var">m</span> <span class="id" title="keyword">as</span> [| <span class="id" title="var">m'</span>] <span class="id" title="var">eqn</span>:<span class="id" title="var">E</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;m&nbsp;=&nbsp;O&nbsp;*)</span> <span class="id" title="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;m&nbsp;=&nbsp;S&nbsp;m'&nbsp;*)</span> <span class="id" title="tactic">discriminate</span> <span class="id" title="var">eq</span>.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;n&nbsp;=&nbsp;S&nbsp;n'&nbsp;*)</span> <span class="id" title="tactic">simpl</span>.<br/>
</div>

<div class="doc">
Notice that both the goal and the induction hypothesis are
    different this time: the goal asks us to prove something more
    general (i.e., to prove the statement for <i>every</i> <span class="inlinecode"><span class="id" title="var">m</span></span>), but the IH
    is correspondingly more flexible, allowing us to choose whichever
    <span class="inlinecode"><span class="id" title="var">m</span></span> we like when we apply the IH. 
</div>
<div class="code">

<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">m</span> <span class="id" title="var">eq</span>.<br/>
</div>

<div class="doc">
Now we've chosen a particular <span class="inlinecode"><span class="id" title="var">m</span></span> and introduced the assumption
    that <span class="inlinecode"><span class="id" title="var">double</span></span> <span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">double</span></span> <span class="inlinecode"><span class="id" title="var">m</span></span>.  Since we are doing a case analysis on
    <span class="inlinecode"><span class="id" title="var">n</span></span>, we also need a case analysis on <span class="inlinecode"><span class="id" title="var">m</span></span> to keep the two "in sync." 
</div>
<div class="code">

<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> <span class="id" title="var">m</span> <span class="id" title="keyword">as</span> [| <span class="id" title="var">m'</span>] <span class="id" title="var">eqn</span>:<span class="id" title="var">E</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;m&nbsp;=&nbsp;O&nbsp;*)</span><br/>
<br/>
</div>

<div class="doc">
The 0 case is trivial: 
</div>
<div class="code">
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">discriminate</span> <span class="id" title="var">eq</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;m&nbsp;=&nbsp;S&nbsp;m'&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <a class="idref" href="Tactics.html#f_equal"><span class="id" title="lemma">f_equal</span></a>.<br/>
</div>

<div class="doc">
At this point, since we are in the second branch of the <span class="inlinecode"><span class="id" title="tactic">destruct</span></span>
    <span class="inlinecode"><span class="id" title="var">m</span></span>, the <span class="inlinecode"><span class="id" title="var">m'</span></span> mentioned in the context is the predecessor of the
    <span class="inlinecode"><span class="id" title="var">m</span></span> we started out talking about.  Since we are also in the <span class="inlinecode"><span class="id" title="var">S</span></span>
    branch of the induction, this is perfect: if we instantiate the
    generic <span class="inlinecode"><span class="id" title="var">m</span></span> in the IH with the current <span class="inlinecode"><span class="id" title="var">m'</span></span> (this instantiation is
    performed automatically by the <span class="inlinecode"><span class="id" title="tactic">apply</span></span> in the next step), then
    <span class="inlinecode"><span class="id" title="var">IHn'</span></span> gives us exactly what we need to finish the proof. 
</div>
<div class="code">

<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <span class="id" title="var">IHn'</span>. <span class="id" title="tactic">simpl</span> <span class="id" title="tactic">in</span> <span class="id" title="var">eq</span>. <span class="id" title="tactic">injection</span> <span class="id" title="var">eq</span> <span class="id" title="keyword">as</span> <span class="id" title="keyword">goal</span>. <span class="id" title="tactic">apply</span> <span class="id" title="keyword">goal</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
What you should take away from all this is that we need to be
    careful, when using induction, that we are not trying to prove
    something too specific: When proving a property involving two
    variables <span class="inlinecode"><span class="id" title="var">n</span></span> and <span class="inlinecode"><span class="id" title="var">m</span></span> by induction on <span class="inlinecode"><span class="id" title="var">n</span></span>, it is sometimes
    crucial to leave <span class="inlinecode"><span class="id" title="var">m</span></span> generic. 
<div class="paragraph"> </div>

 The following exercise follows the same pattern. 
<div class="paragraph"> </div>

<a id="lab150"></a><h4 class="section">Exercise: 2 stars, standard (eqb_true)</h4>

</div>
<div class="code">
<span class="id" title="keyword">Theorem</span> <a id="eqb_true" class="idref" href="#eqb_true"><span class="id" title="lemma">eqb_true</span></a> : <span class="id" title="keyword">∀</span> <a id="n:86" class="idref" href="#n:86"><span class="id" title="binder">n</span></a> <a id="m:87" class="idref" href="#m:87"><span class="id" title="binder">m</span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Tactics.html#n:86"><span class="id" title="variable">n</span></a> <a class="idref" href="Basics.html#ad2ec4e405f68c46c0a176e3e94ae2e<sub>3</sub>"><span class="id" title="notation">=?</span></a> <a class="idref" href="Tactics.html#m:87"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Tactics.html#n:86"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Tactics.html#m:87"><span class="id" title="variable">m</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

<a id="lab151"></a><h4 class="section">Exercise: 2 stars, advanced (eqb_true_informal)</h4>
 Give a careful informal proof of <span class="inlinecode"><span class="id" title="var">eqb_true</span></span>, being as explicit
    as possible about quantifiers. 
</div>
<div class="code">

<br/>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;Do&nbsp;not&nbsp;modify&nbsp;the&nbsp;following&nbsp;line:&nbsp;*)</span><br/>
<span class="id" title="keyword">Definition</span> <a id="manual_grade_for_informal_proof" class="idref" href="#manual_grade_for_informal_proof"><span class="id" title="definition">manual_grade_for_informal_proof</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> (<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a><a class="idref" href="Poly.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">×</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) := <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

<a id="lab152"></a><h4 class="section">Exercise: 3 stars, standard, especially useful (plus_n_n_injective)</h4>
 In addition to being careful about how you use <span class="inlinecode"><span class="id" title="tactic">intros</span></span>, practice
    using "in" variants in this proof.  (Hint: use <span class="inlinecode"><span class="id" title="var">plus_n_Sm</span></span>.) 
</div>
<div class="code">
<span class="id" title="keyword">Theorem</span> <a id="plus_n_n_injective" class="idref" href="#plus_n_n_injective"><span class="id" title="lemma">plus_n_n_injective</span></a> : <span class="id" title="keyword">∀</span> <a id="n:88" class="idref" href="#n:88"><span class="id" title="binder">n</span></a> <a id="m:89" class="idref" href="#m:89"><span class="id" title="binder">m</span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Tactics.html#n:88"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <a class="idref" href="Tactics.html#n:88"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Tactics.html#m:89"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <a class="idref" href="Tactics.html#m:89"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Tactics.html#n:88"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Tactics.html#m:89"><span class="id" title="variable">m</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

 The strategy of doing fewer <span class="inlinecode"><span class="id" title="tactic">intros</span></span> before an <span class="inlinecode"><span class="id" title="tactic">induction</span></span> to
    obtain a more general IH doesn't always work by itself; sometimes
    some <i>rearrangement</i> of quantified variables is needed.  Suppose,
    for example, that we wanted to prove <span class="inlinecode"><span class="id" title="var">double_injective</span></span> by
    induction on <span class="inlinecode"><span class="id" title="var">m</span></span> instead of <span class="inlinecode"><span class="id" title="var">n</span></span>. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Theorem</span> <a id="double_injective_take2_FAILED" class="idref" href="#double_injective_take2_FAILED"><span class="id" title="lemma">double_injective_take2_FAILED</span></a> : <span class="id" title="keyword">∀</span> <a id="n:90" class="idref" href="#n:90"><span class="id" title="binder">n</span></a> <a id="m:91" class="idref" href="#m:91"><span class="id" title="binder">m</span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Induction.html#double"><span class="id" title="definition">double</span></a> <a class="idref" href="Tactics.html#n:90"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Induction.html#double"><span class="id" title="definition">double</span></a> <a class="idref" href="Tactics.html#m:91"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Tactics.html#n:90"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Tactics.html#m:91"><span class="id" title="variable">m</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">n</span> <span class="id" title="var">m</span>. <span class="id" title="tactic">induction</span> <span class="id" title="var">m</span> <span class="id" title="keyword">as</span> [| <span class="id" title="var">m'</span> <span class="id" title="var">IHm'</span>].<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;m&nbsp;=&nbsp;O&nbsp;*)</span> <span class="id" title="tactic">simpl</span>. <span class="id" title="tactic">intros</span> <span class="id" title="var">eq</span>. <span class="id" title="tactic">destruct</span> <span class="id" title="var">n</span> <span class="id" title="keyword">as</span> [| <span class="id" title="var">n'</span>] <span class="id" title="var">eqn</span>:<span class="id" title="var">E</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;n&nbsp;=&nbsp;O&nbsp;*)</span> <span class="id" title="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;n&nbsp;=&nbsp;S&nbsp;n'&nbsp;*)</span> <span class="id" title="tactic">discriminate</span> <span class="id" title="var">eq</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;m&nbsp;=&nbsp;S&nbsp;m'&nbsp;*)</span> <span class="id" title="tactic">intros</span> <span class="id" title="var">eq</span>. <span class="id" title="tactic">destruct</span> <span class="id" title="var">n</span> <span class="id" title="keyword">as</span> [| <span class="id" title="var">n'</span>] <span class="id" title="var">eqn</span>:<span class="id" title="var">E</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;n&nbsp;=&nbsp;O&nbsp;*)</span> <span class="id" title="tactic">discriminate</span> <span class="id" title="var">eq</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;n&nbsp;=&nbsp;S&nbsp;n'&nbsp;*)</span> <span class="id" title="tactic">apply</span> <a class="idref" href="Tactics.html#f_equal"><span class="id" title="lemma">f_equal</span></a>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;Stuck&nbsp;again&nbsp;here,&nbsp;just&nbsp;like&nbsp;before.&nbsp;*)</span><br/>
<span class="id" title="keyword">Abort</span>.<br/>
</div>

<div class="doc">
The problem is that, to do induction on <span class="inlinecode"><span class="id" title="var">m</span></span>, we must first
    introduce <span class="inlinecode"><span class="id" title="var">n</span></span>.  (And if we simply say <span class="inlinecode"><span class="id" title="tactic">induction</span></span> <span class="inlinecode"><span class="id" title="var">m</span></span> without
    introducing anything first, Coq will automatically introduce <span class="inlinecode"><span class="id" title="var">n</span></span>
    for us!)  
<div class="paragraph"> </div>

 What can we do about this?  One possibility is to rewrite the
    statement of the lemma so that <span class="inlinecode"><span class="id" title="var">m</span></span> is quantified before <span class="inlinecode"><span class="id" title="var">n</span></span>.  This
    works, but it's not nice: We don't want to have to twist the
    statements of lemmas to fit the needs of a particular strategy for
    proving them!  Rather we want to state them in the clearest and
    most natural way. 
<div class="paragraph"> </div>

 What we can do instead is to first introduce all the quantified
    variables and then <i>re-generalize</i> one or more of them,
    selectively taking variables out of the context and putting them
    back at the beginning of the goal.  The <span class="inlinecode"><span class="id" title="tactic">generalize</span></span> <span class="inlinecode"><span class="id" title="tactic">dependent</span></span>
    tactic does this. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Theorem</span> <a id="double_injective_take2" class="idref" href="#double_injective_take2"><span class="id" title="lemma">double_injective_take2</span></a> : <span class="id" title="keyword">∀</span> <a id="n:92" class="idref" href="#n:92"><span class="id" title="binder">n</span></a> <a id="m:93" class="idref" href="#m:93"><span class="id" title="binder">m</span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Induction.html#double"><span class="id" title="definition">double</span></a> <a class="idref" href="Tactics.html#n:92"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Induction.html#double"><span class="id" title="definition">double</span></a> <a class="idref" href="Tactics.html#m:93"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Tactics.html#n:92"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Tactics.html#m:93"><span class="id" title="variable">m</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">n</span> <span class="id" title="var">m</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;<span class="inlinecode"><span class="id" title="var">n</span></span>&nbsp;and&nbsp;<span class="inlinecode"><span class="id" title="var">m</span></span>&nbsp;are&nbsp;both&nbsp;in&nbsp;the&nbsp;context&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" title="tactic">generalize</span> <span class="id" title="tactic">dependent</span> <span class="id" title="var">n</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;Now&nbsp;<span class="inlinecode"><span class="id" title="var">n</span></span>&nbsp;is&nbsp;back&nbsp;in&nbsp;the&nbsp;goal&nbsp;and&nbsp;we&nbsp;can&nbsp;do&nbsp;induction&nbsp;on<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">m</span></span>&nbsp;and&nbsp;get&nbsp;a&nbsp;sufficiently&nbsp;general&nbsp;IH.&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" title="tactic">induction</span> <span class="id" title="var">m</span> <span class="id" title="keyword">as</span> [| <span class="id" title="var">m'</span> <span class="id" title="var">IHm'</span>].<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;m&nbsp;=&nbsp;O&nbsp;*)</span> <span class="id" title="tactic">simpl</span>. <span class="id" title="tactic">intros</span> <span class="id" title="var">n</span> <span class="id" title="var">eq</span>. <span class="id" title="tactic">destruct</span> <span class="id" title="var">n</span> <span class="id" title="keyword">as</span> [| <span class="id" title="var">n'</span>] <span class="id" title="var">eqn</span>:<span class="id" title="var">E</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;n&nbsp;=&nbsp;O&nbsp;*)</span> <span class="id" title="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;n&nbsp;=&nbsp;S&nbsp;n'&nbsp;*)</span> <span class="id" title="tactic">discriminate</span> <span class="id" title="var">eq</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;m&nbsp;=&nbsp;S&nbsp;m'&nbsp;*)</span> <span class="id" title="tactic">intros</span> <span class="id" title="var">n</span> <span class="id" title="var">eq</span>. <span class="id" title="tactic">destruct</span> <span class="id" title="var">n</span> <span class="id" title="keyword">as</span> [| <span class="id" title="var">n'</span>] <span class="id" title="var">eqn</span>:<span class="id" title="var">E</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;n&nbsp;=&nbsp;O&nbsp;*)</span> <span class="id" title="tactic">discriminate</span> <span class="id" title="var">eq</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;n&nbsp;=&nbsp;S&nbsp;n'&nbsp;*)</span> <span class="id" title="tactic">apply</span> <a class="idref" href="Tactics.html#f_equal"><span class="id" title="lemma">f_equal</span></a>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <span class="id" title="var">IHm'</span>. <span class="id" title="tactic">injection</span> <span class="id" title="var">eq</span> <span class="id" title="keyword">as</span> <span class="id" title="keyword">goal</span>. <span class="id" title="tactic">apply</span> <span class="id" title="keyword">goal</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
Let's look at an informal proof of this theorem.  Note that
    the proposition we prove by induction leaves <span class="inlinecode"><span class="id" title="var">n</span></span> quantified,
    corresponding to the use of generalize dependent in our formal
    proof.

<div class="paragraph"> </div>

    <i>Theorem</i>: For any nats <span class="inlinecode"><span class="id" title="var">n</span></span> and <span class="inlinecode"><span class="id" title="var">m</span></span>, if <span class="inlinecode"><span class="id" title="var">double</span></span> <span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">double</span></span> <span class="inlinecode"><span class="id" title="var">m</span></span>, then
      <span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">m</span></span>.

<div class="paragraph"> </div>

    <i>Proof</i>: Let <span class="inlinecode"><span class="id" title="var">m</span></span> be a <span class="inlinecode"><span class="id" title="var">nat</span></span>. We prove by induction on <span class="inlinecode"><span class="id" title="var">m</span></span> that, for
      any <span class="inlinecode"><span class="id" title="var">n</span></span>, if <span class="inlinecode"><span class="id" title="var">double</span></span> <span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">double</span></span> <span class="inlinecode"><span class="id" title="var">m</span></span> then <span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">m</span></span>.

<div class="paragraph"> </div>

<ul class="doclist">
<li> First, suppose <span class="inlinecode"><span class="id" title="var">m</span></span> <span class="inlinecode">=</span> <span class="inlinecode">0</span>, and suppose <span class="inlinecode"><span class="id" title="var">n</span></span> is a number such
        that <span class="inlinecode"><span class="id" title="var">double</span></span> <span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">double</span></span> <span class="inlinecode"><span class="id" title="var">m</span></span>.  We must show that <span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode">0</span>.

<div class="paragraph"> </div>

        Since <span class="inlinecode"><span class="id" title="var">m</span></span> <span class="inlinecode">=</span> <span class="inlinecode">0</span>, by the definition of <span class="inlinecode"><span class="id" title="var">double</span></span> we have <span class="inlinecode"><span class="id" title="var">double</span></span> <span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode">=</span>
        <span class="inlinecode">0</span>.  There are two cases to consider for <span class="inlinecode"><span class="id" title="var">n</span></span>.  If <span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode">0</span> we are
        done, since <span class="inlinecode"><span class="id" title="var">m</span></span> <span class="inlinecode">=</span> <span class="inlinecode">0</span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">n</span></span>, as required.  Otherwise, if <span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">S</span></span> <span class="inlinecode"><span class="id" title="var">n'</span></span>
        for some <span class="inlinecode"><span class="id" title="var">n'</span></span>, we derive a contradiction: by the definition of
        <span class="inlinecode"><span class="id" title="var">double</span></span>, we can calculate <span class="inlinecode"><span class="id" title="var">double</span></span> <span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">S</span></span> <span class="inlinecode">(<span class="id" title="var">S</span></span> <span class="inlinecode">(<span class="id" title="var">double</span></span> <span class="inlinecode"><span class="id" title="var">n'</span>))</span>, but
        this contradicts the assumption that <span class="inlinecode"><span class="id" title="var">double</span></span> <span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode">0</span>.

<div class="paragraph"> </div>


</li>
<li> Second, suppose <span class="inlinecode"><span class="id" title="var">m</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">S</span></span> <span class="inlinecode"><span class="id" title="var">m'</span></span> and that <span class="inlinecode"><span class="id" title="var">n</span></span> is again a number such
        that <span class="inlinecode"><span class="id" title="var">double</span></span> <span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">double</span></span> <span class="inlinecode"><span class="id" title="var">m</span></span>.  We must show that <span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">S</span></span> <span class="inlinecode"><span class="id" title="var">m'</span></span>, with
        the induction hypothesis that for every number <span class="inlinecode"><span class="id" title="var">s</span></span>, if <span class="inlinecode"><span class="id" title="var">double</span></span> <span class="inlinecode"><span class="id" title="var">s</span></span> <span class="inlinecode">=</span>
        <span class="inlinecode"><span class="id" title="var">double</span></span> <span class="inlinecode"><span class="id" title="var">m'</span></span> then <span class="inlinecode"><span class="id" title="var">s</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">m'</span></span>.

<div class="paragraph"> </div>

        By the fact that <span class="inlinecode"><span class="id" title="var">m</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">S</span></span> <span class="inlinecode"><span class="id" title="var">m'</span></span> and the definition of <span class="inlinecode"><span class="id" title="var">double</span></span>, we
        have <span class="inlinecode"><span class="id" title="var">double</span></span> <span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">S</span></span> <span class="inlinecode">(<span class="id" title="var">S</span></span> <span class="inlinecode">(<span class="id" title="var">double</span></span> <span class="inlinecode"><span class="id" title="var">m'</span>))</span>.  There are two cases to
        consider for <span class="inlinecode"><span class="id" title="var">n</span></span>.

<div class="paragraph"> </div>

        If <span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode">0</span>, then by definition <span class="inlinecode"><span class="id" title="var">double</span></span> <span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode">0</span>, a contradiction.

<div class="paragraph"> </div>

        Thus, we may assume that <span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">S</span></span> <span class="inlinecode"><span class="id" title="var">n'</span></span> for some <span class="inlinecode"><span class="id" title="var">n'</span></span>, and again by
        the definition of <span class="inlinecode"><span class="id" title="var">double</span></span> we have <span class="inlinecode"><span class="id" title="var">S</span></span> <span class="inlinecode">(<span class="id" title="var">S</span></span> <span class="inlinecode">(<span class="id" title="var">double</span></span> <span class="inlinecode"><span class="id" title="var">n'</span>))</span> <span class="inlinecode">=</span>
        <span class="inlinecode"><span class="id" title="var">S</span></span> <span class="inlinecode">(<span class="id" title="var">S</span></span> <span class="inlinecode">(<span class="id" title="var">double</span></span> <span class="inlinecode"><span class="id" title="var">m'</span>))</span>, which implies by injectivity that <span class="inlinecode"><span class="id" title="var">double</span></span> <span class="inlinecode"><span class="id" title="var">n'</span></span> <span class="inlinecode">=</span>
        <span class="inlinecode"><span class="id" title="var">double</span></span> <span class="inlinecode"><span class="id" title="var">m'</span></span>.  Instantiating the induction hypothesis with <span class="inlinecode"><span class="id" title="var">n'</span></span> thus
        allows us to conclude that <span class="inlinecode"><span class="id" title="var">n'</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">m'</span></span>, and it follows immediately
        that <span class="inlinecode"><span class="id" title="var">S</span></span> <span class="inlinecode"><span class="id" title="var">n'</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">S</span></span> <span class="inlinecode"><span class="id" title="var">m'</span></span>.  Since <span class="inlinecode"><span class="id" title="var">S</span></span> <span class="inlinecode"><span class="id" title="var">n'</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">n</span></span> and <span class="inlinecode"><span class="id" title="var">S</span></span> <span class="inlinecode"><span class="id" title="var">m'</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">m</span></span>, this is just
        what we wanted to show. <font size=-2>&#9744;</font> 
</li>
</ul>

<div class="paragraph"> </div>

<a id="lab153"></a><h4 class="section">Exercise: 3 stars, standard, especially useful (gen_dep_practice)</h4>
 Prove this by induction on <span class="inlinecode"><span class="id" title="var">l</span></span>. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Theorem</span> <a id="nth_error_after_last" class="idref" href="#nth_error_after_last"><span class="id" title="lemma">nth_error_after_last</span></a>: <span class="id" title="keyword">∀</span> (<a id="n:94" class="idref" href="#n:94"><span class="id" title="binder">n</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) (<a id="X:95" class="idref" href="#X:95"><span class="id" title="binder">X</span></a> : <span class="id" title="keyword">Type</span>) (<a id="l:96" class="idref" href="#l:96"><span class="id" title="binder">l</span></a> : <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Tactics.html#X:95"><span class="id" title="variable">X</span></a>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Poly.html#length"><span class="id" title="definition">length</span></a> <a class="idref" href="Tactics.html#l:96"><span class="id" title="variable">l</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Tactics.html#n:94"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Poly.html#nth_error"><span class="id" title="definition">nth_error</span></a> <a class="idref" href="Tactics.html#l:96"><span class="id" title="variable">l</span></a> <a class="idref" href="Tactics.html#n:94"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>


<div class="doc">
<a id="lab154"></a><h1 class="section">Unfolding Definitions</h1>

<div class="paragraph"> </div>

 It sometimes happens that we need to manually unfold a name that
    has been introduced by a <span class="inlinecode"><span class="id" title="keyword">Definition</span></span> so that we can manipulate
    the expression it denotes.  For example, if we define... 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Definition</span> <a id="square" class="idref" href="#square"><span class="id" title="definition">square</span></a> <a id="n:97" class="idref" href="#n:97"><span class="id" title="binder">n</span></a> := <a class="idref" href="Tactics.html#n:97"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc<sub>54</sub>"><span class="id" title="notation">×</span></a> <a class="idref" href="Tactics.html#n:97"><span class="id" title="variable">n</span></a>.<br/>
</div>

<div class="doc">
... and try to prove a simple fact about <span class="inlinecode"><span class="id" title="var">square</span></span>... 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Lemma</span> <a id="square_mult" class="idref" href="#square_mult"><span class="id" title="lemma">square_mult</span></a> : <span class="id" title="keyword">∀</span> <a id="n:98" class="idref" href="#n:98"><span class="id" title="binder">n</span></a> <a id="m:99" class="idref" href="#m:99"><span class="id" title="binder">m</span></a>, <a class="idref" href="Tactics.html#square"><span class="id" title="definition">square</span></a> (<a class="idref" href="Tactics.html#n:98"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc<sub>54</sub>"><span class="id" title="notation">×</span></a> <a class="idref" href="Tactics.html#m:99"><span class="id" title="variable">m</span></a>) <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Tactics.html#square"><span class="id" title="definition">square</span></a> <a class="idref" href="Tactics.html#n:98"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc<sub>54</sub>"><span class="id" title="notation">×</span></a> <a class="idref" href="Tactics.html#square"><span class="id" title="definition">square</span></a> <a class="idref" href="Tactics.html#m:99"><span class="id" title="variable">m</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">n</span> <span class="id" title="var">m</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">simpl</span>.<br/>
</div>

<div class="doc">
... we appear to be stuck: <span class="inlinecode"><span class="id" title="tactic">simpl</span></span> doesn't simplify anything, and
    since we haven't proved any other facts about <span class="inlinecode"><span class="id" title="var">square</span></span>, there is
    nothing we can <span class="inlinecode"><span class="id" title="tactic">apply</span></span> or <span class="inlinecode"><span class="id" title="tactic">rewrite</span></span> with. 
<div class="paragraph"> </div>

  To make progress, we can manually <span class="inlinecode"><span class="id" title="tactic">unfold</span></span> the definition of
    <span class="inlinecode"><span class="id" title="var">square</span></span>: 
</div>
<div class="code">

<br/>
&nbsp;&nbsp;<span class="id" title="tactic">unfold</span> <a class="idref" href="Tactics.html#square"><span class="id" title="definition">square</span></a>.<br/>
</div>

<div class="doc">
Now we have plenty to work with: both sides of the equality are
    expressions involving multiplication, and we have lots of facts
    about multiplication at our disposal.  In particular, we know that
    it is commutative and associative, and from these it is not hard
    to finish the proof. 
</div>
<div class="code">

<br/>
&nbsp;&nbsp;<span class="id" title="tactic">rewrite</span> <a class="idref" href="Induction.html#mult_assoc"><span class="id" title="axiom">mult_assoc</span></a>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">assert</span> (<span class="id" title="var">H</span> : <span class="id" title="var">n</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc<sub>54</sub>"><span class="id" title="notation">×</span></a> <span class="id" title="var">m</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc<sub>54</sub>"><span class="id" title="notation">×</span></a> <span class="id" title="var">n</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <span class="id" title="var">n</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc<sub>54</sub>"><span class="id" title="notation">×</span></a> <span class="id" title="var">n</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc<sub>54</sub>"><span class="id" title="notation">×</span></a> <span class="id" title="var">m</span>).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;{ <span class="id" title="tactic">rewrite</span> <a class="idref" href="Induction.html#mult_comm"><span class="id" title="axiom">mult_comm</span></a>. <span class="id" title="tactic">apply</span> <a class="idref" href="Induction.html#mult_assoc"><span class="id" title="axiom">mult_assoc</span></a>. }<br/>
&nbsp;&nbsp;<span class="id" title="tactic">rewrite</span> <span class="id" title="var">H</span>. <span class="id" title="tactic">rewrite</span> <a class="idref" href="Induction.html#mult_assoc"><span class="id" title="axiom">mult_assoc</span></a>. <span class="id" title="tactic">reflexivity</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
At this point, some discussion of unfolding and simplification is
    in order.

<div class="paragraph"> </div>

    We already have observed that tactics like <span class="inlinecode"><span class="id" title="tactic">simpl</span></span>, <span class="inlinecode"><span class="id" title="tactic">reflexivity</span></span>,
    and <span class="inlinecode"><span class="id" title="tactic">apply</span></span> will often unfold the definitions of functions
    automatically when this allows them to make progress.  For
    example, if we define <span class="inlinecode"><span class="id" title="var">foo</span></span> <span class="inlinecode"><span class="id" title="var">m</span></span> to be the constant <span class="inlinecode">5</span>... 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Definition</span> <a id="foo" class="idref" href="#foo"><span class="id" title="definition">foo</span></a> (<a id="x:100" class="idref" href="#x:100"><span class="id" title="binder">x</span></a>: <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) := 5.<br/>
</div>

<div class="doc">
.... then the <span class="inlinecode"><span class="id" title="tactic">simpl</span></span> in the following proof (or the
    <span class="inlinecode"><span class="id" title="tactic">reflexivity</span></span>, if we omit the <span class="inlinecode"><span class="id" title="tactic">simpl</span></span>) will unfold <span class="inlinecode"><span class="id" title="var">foo</span></span> <span class="inlinecode"><span class="id" title="var">m</span></span> to
    <span class="inlinecode">(<span class="id" title="keyword">fun</span></span> <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode">⇒</span> <span class="inlinecode">5)</span> <span class="inlinecode"><span class="id" title="var">m</span></span> and then further simplify this expression to just
    <span class="inlinecode">5</span>. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Fact</span> <a id="silly_fact_1" class="idref" href="#silly_fact_1"><span class="id" title="lemma">silly_fact_1</span></a> : <span class="id" title="keyword">∀</span> <a id="m:101" class="idref" href="#m:101"><span class="id" title="binder">m</span></a>, <a class="idref" href="Tactics.html#foo"><span class="id" title="definition">foo</span></a> <a class="idref" href="Tactics.html#m:101"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> 1 <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Tactics.html#foo"><span class="id" title="definition">foo</span></a> (<a class="idref" href="Tactics.html#m:101"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> 1) <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> 1.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">m</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">simpl</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">reflexivity</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
However, this automatic unfolding is somewhat conservative.  For
    example, if we define a slightly more complicated function
    involving a pattern match... 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Definition</span> <a id="bar" class="idref" href="#bar"><span class="id" title="definition">bar</span></a> <a id="x:102" class="idref" href="#x:102"><span class="id" title="binder">x</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Tactics.html#x:102"><span class="id" title="variable">x</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#O"><span class="id" title="constructor">O</span></a> ⇒ 5<br/>
&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <span class="id" title="var">_</span> ⇒ 5<br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>
</div>

<div class="doc">
...then the analogous proof will get stuck: 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Fact</span> <a id="silly_fact_2_FAILED" class="idref" href="#silly_fact_2_FAILED"><span class="id" title="lemma">silly_fact_2_FAILED</span></a> : <span class="id" title="keyword">∀</span> <a id="m:104" class="idref" href="#m:104"><span class="id" title="binder">m</span></a>, <a class="idref" href="Tactics.html#bar"><span class="id" title="definition">bar</span></a> <a class="idref" href="Tactics.html#m:104"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> 1 <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Tactics.html#bar"><span class="id" title="definition">bar</span></a> (<a class="idref" href="Tactics.html#m:104"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> 1) <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> 1.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">m</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">simpl</span>. <span class="comment">(*&nbsp;Does&nbsp;nothing!&nbsp;*)</span><br/>
<span class="id" title="keyword">Abort</span>.<br/>
</div>

<div class="doc">
The reason that <span class="inlinecode"><span class="id" title="tactic">simpl</span></span> doesn't make progress here is that it
    notices that, after tentatively unfolding <span class="inlinecode"><span class="id" title="var">bar</span></span> <span class="inlinecode"><span class="id" title="var">m</span></span>, it is left with
    a match whose scrutinee, <span class="inlinecode"><span class="id" title="var">m</span></span>, is a variable, so the <span class="inlinecode"><span class="id" title="keyword">match</span></span> cannot
    be simplified further.  It is not smart enough to notice that the
    two branches of the <span class="inlinecode"><span class="id" title="keyword">match</span></span> are identical, so it gives up on
    unfolding <span class="inlinecode"><span class="id" title="var">bar</span></span> <span class="inlinecode"><span class="id" title="var">m</span></span> and leaves it alone.  Similarly, tentatively
    unfolding <span class="inlinecode"><span class="id" title="var">bar</span></span> <span class="inlinecode">(<span class="id" title="var">m</span>+1)</span> leaves a <span class="inlinecode"><span class="id" title="keyword">match</span></span> whose scrutinee is a
    function application (that cannot itself be simplified, even
    after unfolding the definition of <span class="inlinecode">+</span>), so <span class="inlinecode"><span class="id" title="tactic">simpl</span></span> leaves it
    alone. 
<div class="paragraph"> </div>

 At this point, there are two ways to make progress.  One is to use
    <span class="inlinecode"><span class="id" title="tactic">destruct</span></span> <span class="inlinecode"><span class="id" title="var">m</span></span> to break the proof into two cases, each focusing on a
    more concrete choice of <span class="inlinecode"><span class="id" title="var">m</span></span> (<span class="inlinecode"><span class="id" title="var">O</span></span> vs <span class="inlinecode"><span class="id" title="var">S</span></span> <span class="inlinecode"><span class="id" title="var">_</span></span>).  In each case, the
    <span class="inlinecode"><span class="id" title="keyword">match</span></span> inside of <span class="inlinecode"><span class="id" title="var">bar</span></span> can now make progress, and the proof is
    easy to complete. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Fact</span> <a id="silly_fact_2" class="idref" href="#silly_fact_2"><span class="id" title="lemma">silly_fact_2</span></a> : <span class="id" title="keyword">∀</span> <a id="m:105" class="idref" href="#m:105"><span class="id" title="binder">m</span></a>, <a class="idref" href="Tactics.html#bar"><span class="id" title="definition">bar</span></a> <a class="idref" href="Tactics.html#m:105"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> 1 <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Tactics.html#bar"><span class="id" title="definition">bar</span></a> (<a class="idref" href="Tactics.html#m:105"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> 1) <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> 1.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">m</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> <span class="id" title="var">m</span> <span class="id" title="var">eqn</span>:<span class="id" title="var">E</span>.<br/>
&nbsp;&nbsp;- <span class="id" title="tactic">simpl</span>. <span class="id" title="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="id" title="tactic">simpl</span>. <span class="id" title="tactic">reflexivity</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
This approach works, but it depends on our recognizing that the
    <span class="inlinecode"><span class="id" title="keyword">match</span></span> hidden inside <span class="inlinecode"><span class="id" title="var">bar</span></span> is what was preventing us from making
    progress. 
<div class="paragraph"> </div>

 A more straightforward way forward is to explicitly tell Coq to
    unfold <span class="inlinecode"><span class="id" title="var">bar</span></span>. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Fact</span> <a id="silly_fact_2'" class="idref" href="#silly_fact_2'"><span class="id" title="lemma">silly_fact_2'</span></a> : <span class="id" title="keyword">∀</span> <a id="m:106" class="idref" href="#m:106"><span class="id" title="binder">m</span></a>, <a class="idref" href="Tactics.html#bar"><span class="id" title="definition">bar</span></a> <a class="idref" href="Tactics.html#m:106"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> 1 <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Tactics.html#bar"><span class="id" title="definition">bar</span></a> (<a class="idref" href="Tactics.html#m:106"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> 1) <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> 1.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">m</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">unfold</span> <a class="idref" href="Tactics.html#bar"><span class="id" title="definition">bar</span></a>.<br/>
</div>

<div class="doc">
Now it is apparent that we are stuck on the <span class="inlinecode"><span class="id" title="keyword">match</span></span> expressions on
    both sides of the <span class="inlinecode">=</span>, and we can use <span class="inlinecode"><span class="id" title="tactic">destruct</span></span> to finish the
    proof without thinking too hard. 
</div>
<div class="code">

<br/>
&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> <span class="id" title="var">m</span> <span class="id" title="var">eqn</span>:<span class="id" title="var">E</span>.<br/>
&nbsp;&nbsp;- <span class="id" title="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="id" title="tactic">reflexivity</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a id="lab155"></a><h1 class="section">Using <span class="inlinecode"><span class="id" title="tactic">destruct</span></span> on Compound Expressions</h1>

<div class="paragraph"> </div>

 We have seen many examples where <span class="inlinecode"><span class="id" title="tactic">destruct</span></span> is used to
    perform case analysis of the value of some variable.  Sometimes we
    need to reason by cases on the result of some <i>expression</i>.  We
    can also do this with <span class="inlinecode"><span class="id" title="tactic">destruct</span></span>.

<div class="paragraph"> </div>

    Here are some examples: 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Definition</span> <a id="sillyfun" class="idref" href="#sillyfun"><span class="id" title="definition">sillyfun</span></a> (<a id="n:107" class="idref" href="#n:107"><span class="id" title="binder">n</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) : <a class="idref" href="Basics.html#bool"><span class="id" title="inductive">bool</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">if</span> <a class="idref" href="Tactics.html#n:107"><span class="id" title="variable">n</span></a> <a class="idref" href="Basics.html#ad2ec4e405f68c46c0a176e3e94ae2e<sub>3</sub>"><span class="id" title="notation">=?</span></a> 3 <span class="id" title="keyword">then</span> <a class="idref" href="Basics.html#false"><span class="id" title="constructor">false</span></a><br/>
&nbsp;&nbsp;<span class="id" title="keyword">else</span> <span class="id" title="keyword">if</span> <a class="idref" href="Tactics.html#n:107"><span class="id" title="variable">n</span></a> <a class="idref" href="Basics.html#ad2ec4e405f68c46c0a176e3e94ae2e<sub>3</sub>"><span class="id" title="notation">=?</span></a> 5 <span class="id" title="keyword">then</span> <a class="idref" href="Basics.html#false"><span class="id" title="constructor">false</span></a><br/>
&nbsp;&nbsp;<span class="id" title="keyword">else</span> <a class="idref" href="Basics.html#false"><span class="id" title="constructor">false</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Theorem</span> <a id="sillyfun_false" class="idref" href="#sillyfun_false"><span class="id" title="lemma">sillyfun_false</span></a> : <span class="id" title="keyword">∀</span> (<a id="n:108" class="idref" href="#n:108"><span class="id" title="binder">n</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>),<br/>
&nbsp;&nbsp;<a class="idref" href="Tactics.html#sillyfun"><span class="id" title="definition">sillyfun</span></a> <a class="idref" href="Tactics.html#n:108"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Basics.html#false"><span class="id" title="constructor">false</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">n</span>. <span class="id" title="tactic">unfold</span> <a class="idref" href="Tactics.html#sillyfun"><span class="id" title="definition">sillyfun</span></a>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> (<span class="id" title="var">n</span> <a class="idref" href="Basics.html#ad2ec4e405f68c46c0a176e3e94ae2e<sub>3</sub>"><span class="id" title="notation">=?</span></a> 3) <span class="id" title="var">eqn</span>:<span class="id" title="var">E<sub>1</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;- <span class="comment">(*&nbsp;n&nbsp;=?&nbsp;3&nbsp;=&nbsp;true&nbsp;*)</span> <span class="id" title="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;- <span class="comment">(*&nbsp;n&nbsp;=?&nbsp;3&nbsp;=&nbsp;false&nbsp;*)</span> <span class="id" title="tactic">destruct</span> (<span class="id" title="var">n</span> <a class="idref" href="Basics.html#ad2ec4e405f68c46c0a176e3e94ae2e<sub>3</sub>"><span class="id" title="notation">=?</span></a> 5) <span class="id" title="var">eqn</span>:<span class="id" title="var">E<sub>2</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;n&nbsp;=?&nbsp;5&nbsp;=&nbsp;true&nbsp;*)</span> <span class="id" title="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;n&nbsp;=?&nbsp;5&nbsp;=&nbsp;false&nbsp;*)</span> <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
After unfolding <span class="inlinecode"><span class="id" title="var">sillyfun</span></span> in the above proof, we find that
    we are stuck on <span class="inlinecode"><span class="id" title="keyword">if</span></span> <span class="inlinecode">(<span class="id" title="var">n</span></span> <span class="inlinecode">=?</span> <span class="inlinecode">3)</span> <span class="inlinecode"><span class="id" title="keyword">then</span></span> <span class="inlinecode">...</span> <span class="inlinecode"><span class="id" title="keyword">else</span></span> <span class="inlinecode">...</span>.  But either
    <span class="inlinecode"><span class="id" title="var">n</span></span> is equal to <span class="inlinecode">3</span> or it isn't, so we can use <span class="inlinecode"><span class="id" title="tactic">destruct</span></span> <span class="inlinecode">(<span class="id" title="var">eqb</span></span>
    <span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode">3)</span> to let us reason about the two cases.

<div class="paragraph"> </div>

    In general, the <span class="inlinecode"><span class="id" title="tactic">destruct</span></span> tactic can be used to perform case
    analysis of the results of arbitrary computations.  If <span class="inlinecode"><span class="id" title="var">e</span></span> is an
    expression whose type is some inductively defined type <span class="inlinecode"><span class="id" title="var">T</span></span>, then,
    for each constructor <span class="inlinecode"><span class="id" title="var">c</span></span> of <span class="inlinecode"><span class="id" title="var">T</span></span>, <span class="inlinecode"><span class="id" title="tactic">destruct</span></span> <span class="inlinecode"><span class="id" title="var">e</span></span> generates a subgoal
    in which all occurrences of <span class="inlinecode"><span class="id" title="var">e</span></span> (in the goal and in the context)
    are replaced by <span class="inlinecode"><span class="id" title="var">c</span></span>. 
<div class="paragraph"> </div>

<a id="lab156"></a><h4 class="section">Exercise: 3 stars, standard (combine_split)</h4>
 Here is an implementation of the <span class="inlinecode"><span class="id" title="tactic">split</span></span> function mentioned in
    chapter <a href="Poly.html"><span class="inlineref">Poly</span></a>: 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Fixpoint</span> <a id="split" class="idref" href="#split"><span class="id" title="definition">split</span></a> {<a id="X:109" class="idref" href="#X:109"><span class="id" title="binder">X</span></a> <a id="Y:110" class="idref" href="#Y:110"><span class="id" title="binder">Y</span></a> : <span class="id" title="keyword">Type</span>} (<a id="l:111" class="idref" href="#l:111"><span class="id" title="binder">l</span></a> : <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> (<a class="idref" href="Tactics.html#X:109"><span class="id" title="variable">X</span></a><a class="idref" href="Poly.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">×</span></a><a class="idref" href="Tactics.html#Y:110"><span class="id" title="variable">Y</span></a>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: <a class="idref" href="Poly.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Tactics.html#X:109"><span class="id" title="variable">X</span></a><a class="idref" href="Poly.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">)</span></a> <a class="idref" href="Poly.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">×</span></a> <a class="idref" href="Poly.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Tactics.html#Y:110"><span class="id" title="variable">Y</span></a><a class="idref" href="Poly.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">)</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Tactics.html#l:111"><span class="id" title="variable">l</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="Poly.html#2c60282cbb04e070c60ae01e76f3865a"><span class="id" title="notation">[]</span></a> ⇒ <a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="Poly.html#2c60282cbb04e070c60ae01e76f3865a"><span class="id" title="notation">[]</span></a><a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">,</span></a> <a class="idref" href="Poly.html#2c60282cbb04e070c60ae01e76f3865a"><span class="id" title="notation">[]</span></a><a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;| <a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">(</span></a><span class="id" title="var">x</span><a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">,</span></a> <span class="id" title="var">y</span><a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">)</span></a> <a class="idref" href="Poly.html#:::x_'::'_x"><span class="id" title="notation">::</span></a> <span class="id" title="var">t</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Tactics.html#split:112"><span class="id" title="definition">split</span></a> <span class="id" title="var">t</span> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">(</span></a><span class="id" title="var">lx</span><a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">,</span></a> <span class="id" title="var">ly</span><a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">)</span></a> ⇒ <a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">(</span></a><span class="id" title="var">x</span> <a class="idref" href="Poly.html#:::x_'::'_x"><span class="id" title="notation">::</span></a> <span class="id" title="var">lx</span><a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">,</span></a> <span class="id" title="var">y</span> <a class="idref" href="Poly.html#:::x_'::'_x"><span class="id" title="notation">::</span></a> <span class="id" title="var">ly</span><a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">end</span><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>
</div>

<div class="doc">
Prove that <span class="inlinecode"><span class="id" title="tactic">split</span></span> and <span class="inlinecode"><span class="id" title="var">combine</span></span> are inverses in the following
    sense: 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Theorem</span> <a id="combine_split" class="idref" href="#combine_split"><span class="id" title="lemma">combine_split</span></a> : <span class="id" title="keyword">∀</span> <a id="X:114" class="idref" href="#X:114"><span class="id" title="binder">X</span></a> <a id="Y:115" class="idref" href="#Y:115"><span class="id" title="binder">Y</span></a> (<a id="l:116" class="idref" href="#l:116"><span class="id" title="binder">l</span></a> : <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> (<a class="idref" href="Tactics.html#X:114"><span class="id" title="variable">X</span></a> <a class="idref" href="Poly.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">×</span></a> <a class="idref" href="Tactics.html#Y:115"><span class="id" title="variable">Y</span></a>)) <a id="l<sub>1</sub>:117" class="idref" href="#l<sub>1</sub>:117"><span class="id" title="binder">l<sub>1</sub></span></a> <a id="l<sub>2</sub>:118" class="idref" href="#l<sub>2</sub>:118"><span class="id" title="binder">l<sub>2</sub></span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="Tactics.html#split"><span class="id" title="definition">split</span></a> <a class="idref" href="Tactics.html#l:116"><span class="id" title="variable">l</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="Tactics.html#l<sub>1</sub>:117"><span class="id" title="variable">l<sub>1</sub></span></a><a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">,</span></a> <a class="idref" href="Tactics.html#l<sub>2</sub>:118"><span class="id" title="variable">l<sub>2</sub></span></a><a class="idref" href="Poly.html#62264328926d76449e4f268ee9289ca<sub>9</sub>"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="Poly.html#combine"><span class="id" title="definition">combine</span></a> <a class="idref" href="Tactics.html#l<sub>1</sub>:117"><span class="id" title="variable">l<sub>1</sub></span></a> <a class="idref" href="Tactics.html#l<sub>2</sub>:118"><span class="id" title="variable">l<sub>2</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Tactics.html#l:116"><span class="id" title="variable">l</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

 The <span class="inlinecode"><span class="id" title="var">eqn</span>:</span> part of the <span class="inlinecode"><span class="id" title="tactic">destruct</span></span> tactic is optional: So far,
    we've chosen to include it most of the time, just for the sake of
    documentation.

<div class="paragraph"> </div>

    However, when <span class="inlinecode"><span class="id" title="tactic">destruct</span></span>ing compound expressions, the information
    recorded by the <span class="inlinecode"><span class="id" title="var">eqn</span>:</span> can actually be critical: if we leave it
    out, then <span class="inlinecode"><span class="id" title="tactic">destruct</span></span> can erase information we need to complete a
    proof.  For example, suppose we define a function <span class="inlinecode"><span class="id" title="var">sillyfun1</span></span> like
    this: 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Definition</span> <a id="sillyfun1" class="idref" href="#sillyfun1"><span class="id" title="definition">sillyfun1</span></a> (<a id="n:119" class="idref" href="#n:119"><span class="id" title="binder">n</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) : <a class="idref" href="Basics.html#bool"><span class="id" title="inductive">bool</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">if</span> <a class="idref" href="Tactics.html#n:119"><span class="id" title="variable">n</span></a> <a class="idref" href="Basics.html#ad2ec4e405f68c46c0a176e3e94ae2e<sub>3</sub>"><span class="id" title="notation">=?</span></a> 3 <span class="id" title="keyword">then</span> <a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a><br/>
&nbsp;&nbsp;<span class="id" title="keyword">else</span> <span class="id" title="keyword">if</span> <a class="idref" href="Tactics.html#n:119"><span class="id" title="variable">n</span></a> <a class="idref" href="Basics.html#ad2ec4e405f68c46c0a176e3e94ae2e<sub>3</sub>"><span class="id" title="notation">=?</span></a> 5 <span class="id" title="keyword">then</span> <a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a><br/>
&nbsp;&nbsp;<span class="id" title="keyword">else</span> <a class="idref" href="Basics.html#false"><span class="id" title="constructor">false</span></a>.<br/>
</div>

<div class="doc">
Now suppose that we want to convince Coq that <span class="inlinecode"><span class="id" title="var">sillyfun1</span></span> <span class="inlinecode"><span class="id" title="var">n</span></span>
    yields <span class="inlinecode"><span class="id" title="var">true</span></span> only when <span class="inlinecode"><span class="id" title="var">n</span></span> is odd.  If we start the proof like
    this (with no <span class="inlinecode"><span class="id" title="var">eqn</span>:</span> on the <span class="inlinecode"><span class="id" title="tactic">destruct</span></span>)... 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Theorem</span> <a id="sillyfun1_odd_FAILED" class="idref" href="#sillyfun1_odd_FAILED"><span class="id" title="lemma">sillyfun1_odd_FAILED</span></a> : <span class="id" title="keyword">∀</span> (<a id="n:120" class="idref" href="#n:120"><span class="id" title="binder">n</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Tactics.html#sillyfun1"><span class="id" title="definition">sillyfun1</span></a> <a class="idref" href="Tactics.html#n:120"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Basics.html#oddb"><span class="id" title="definition">oddb</span></a> <a class="idref" href="Tactics.html#n:120"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">n</span> <span class="id" title="var">eq</span>. <span class="id" title="tactic">unfold</span> <a class="idref" href="Tactics.html#sillyfun1"><span class="id" title="definition">sillyfun1</span></a> <span class="id" title="tactic">in</span> <span class="id" title="var">eq</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> (<span class="id" title="var">n</span> <a class="idref" href="Basics.html#ad2ec4e405f68c46c0a176e3e94ae2e<sub>3</sub>"><span class="id" title="notation">=?</span></a> 3).<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;stuck...&nbsp;*)</span><br/>
<span class="id" title="keyword">Abort</span>.<br/>
</div>

<div class="doc">
... then we are stuck at this point because the context does
    not contain enough information to prove the goal!  The problem is
    that the substitution performed by <span class="inlinecode"><span class="id" title="tactic">destruct</span></span> is quite brutal --
    in this case, it throws away every occurrence of <span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode">=?</span> <span class="inlinecode">3</span>, but we
    need to keep some memory of this expression and how it was
    destructed, because we need to be able to reason that, since <span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode">=?</span>
    <span class="inlinecode">3</span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">true</span></span> in this branch of the case analysis, it must be that <span class="inlinecode"><span class="id" title="var">n</span></span>
    <span class="inlinecode">=</span> <span class="inlinecode">3</span>, from which it follows that <span class="inlinecode"><span class="id" title="var">n</span></span> is odd.

<div class="paragraph"> </div>

    What we want here is to substitute away all existing occurences of
    <span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode">=?</span> <span class="inlinecode">3</span>, but at the same time add an equation to the context that
    records which case we are in.  This is precisely what the <span class="inlinecode"><span class="id" title="var">eqn</span>:</span>
    qualifier does. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Theorem</span> <a id="sillyfun1_odd" class="idref" href="#sillyfun1_odd"><span class="id" title="lemma">sillyfun1_odd</span></a> : <span class="id" title="keyword">∀</span> (<a id="n:121" class="idref" href="#n:121"><span class="id" title="binder">n</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Tactics.html#sillyfun1"><span class="id" title="definition">sillyfun1</span></a> <a class="idref" href="Tactics.html#n:121"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Basics.html#oddb"><span class="id" title="definition">oddb</span></a> <a class="idref" href="Tactics.html#n:121"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">n</span> <span class="id" title="var">eq</span>. <span class="id" title="tactic">unfold</span> <a class="idref" href="Tactics.html#sillyfun1"><span class="id" title="definition">sillyfun1</span></a> <span class="id" title="tactic">in</span> <span class="id" title="var">eq</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> (<span class="id" title="var">n</span> <a class="idref" href="Basics.html#ad2ec4e405f68c46c0a176e3e94ae2e<sub>3</sub>"><span class="id" title="notation">=?</span></a> 3) <span class="id" title="var">eqn</span>:<span class="id" title="var">Heqe3</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;Now&nbsp;we&nbsp;have&nbsp;the&nbsp;same&nbsp;state&nbsp;as&nbsp;at&nbsp;the&nbsp;point&nbsp;where&nbsp;we&nbsp;got<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;stuck&nbsp;above,&nbsp;except&nbsp;that&nbsp;the&nbsp;context&nbsp;contains&nbsp;an&nbsp;extra<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;equality&nbsp;assumption,&nbsp;which&nbsp;is&nbsp;exactly&nbsp;what&nbsp;we&nbsp;need&nbsp;to<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;make&nbsp;progress.&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;- <span class="comment">(*&nbsp;e<sub>3</sub>&nbsp;=&nbsp;true&nbsp;*)</span> <span class="id" title="tactic">apply</span> <a class="idref" href="Tactics.html#eqb_true"><span class="id" title="axiom">eqb_true</span></a> <span class="id" title="tactic">in</span> <span class="id" title="var">Heqe3</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">rewrite</span> → <span class="id" title="var">Heqe3</span>. <span class="id" title="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;- <span class="comment">(*&nbsp;e<sub>3</sub>&nbsp;=&nbsp;false&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;When&nbsp;we&nbsp;come&nbsp;to&nbsp;the&nbsp;second&nbsp;equality&nbsp;test&nbsp;in&nbsp;the&nbsp;body<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;of&nbsp;the&nbsp;function&nbsp;we&nbsp;are&nbsp;reasoning&nbsp;about,&nbsp;we&nbsp;can&nbsp;use<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="inlinecode"><span class="id" title="var">eqn</span>:</span>&nbsp;again&nbsp;in&nbsp;the&nbsp;same&nbsp;way,&nbsp;allowing&nbsp;us&nbsp;to&nbsp;finish&nbsp;the<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;proof.&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> (<span class="id" title="var">n</span> <a class="idref" href="Basics.html#ad2ec4e405f68c46c0a176e3e94ae2e<sub>3</sub>"><span class="id" title="notation">=?</span></a> 5) <span class="id" title="var">eqn</span>:<span class="id" title="var">Heqe5</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;e<sub>5</sub>&nbsp;=&nbsp;true&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <a class="idref" href="Tactics.html#eqb_true"><span class="id" title="axiom">eqb_true</span></a> <span class="id" title="tactic">in</span> <span class="id" title="var">Heqe5</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">rewrite</span> → <span class="id" title="var">Heqe5</span>. <span class="id" title="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;e<sub>5</sub>&nbsp;=&nbsp;false&nbsp;*)</span> <span class="id" title="tactic">discriminate</span> <span class="id" title="var">eq</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a id="lab157"></a><h4 class="section">Exercise: 2 stars, standard (destruct_eqn_practice)</h4>

</div>
<div class="code">
<span class="id" title="keyword">Theorem</span> <a id="bool_fn_applied_thrice" class="idref" href="#bool_fn_applied_thrice"><span class="id" title="lemma">bool_fn_applied_thrice</span></a> :<br/>
&nbsp;&nbsp;<span class="id" title="keyword">∀</span> (<a id="f:122" class="idref" href="#f:122"><span class="id" title="binder">f</span></a> : <a class="idref" href="Basics.html#bool"><span class="id" title="inductive">bool</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Basics.html#bool"><span class="id" title="inductive">bool</span></a>) (<a id="b:123" class="idref" href="#b:123"><span class="id" title="binder">b</span></a> : <a class="idref" href="Basics.html#bool"><span class="id" title="inductive">bool</span></a>),<br/>
&nbsp;&nbsp;<a class="idref" href="Tactics.html#f:122"><span class="id" title="variable">f</span></a> (<a class="idref" href="Tactics.html#f:122"><span class="id" title="variable">f</span></a> (<a class="idref" href="Tactics.html#f:122"><span class="id" title="variable">f</span></a> <a class="idref" href="Tactics.html#b:123"><span class="id" title="variable">b</span></a>)) <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Tactics.html#f:122"><span class="id" title="variable">f</span></a> <a class="idref" href="Tactics.html#b:123"><span class="id" title="variable">b</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>


<div class="doc">
<a id="lab158"></a><h1 class="section">Review</h1>

<div class="paragraph"> </div>

 We've now seen many of Coq's most fundamental tactics.  We'll
    introduce a few more in the coming chapters, and later on we'll
    see some more powerful <i>automation</i> tactics that make Coq help us
    with low-level details.  But basically we've got what we need to
    get work done.

<div class="paragraph"> </div>

    Here are the ones we've seen:

<div class="paragraph"> </div>

<ul class="doclist">
<li> <span class="inlinecode"><span class="id" title="tactic">intros</span></span>: move hypotheses/variables from goal to context

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" title="tactic">reflexivity</span></span>: finish the proof (when the goal looks like <span class="inlinecode"><span class="id" title="var">e</span></span> <span class="inlinecode">=</span>
        <span class="inlinecode"><span class="id" title="var">e</span></span>)

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" title="tactic">apply</span></span>: prove goal using a hypothesis, lemma, or constructor

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" title="tactic">apply</span>...</span> <span class="inlinecode"><span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">H</span></span>: apply a hypothesis, lemma, or constructor to
        a hypothesis in the context (forward reasoning)

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" title="tactic">apply</span>...</span> <span class="inlinecode"><span class="id" title="keyword">with</span>...</span>: explicitly specify values for variables
        that cannot be determined by pattern matching

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" title="tactic">simpl</span></span>: simplify computations in the goal

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" title="tactic">simpl</span></span> <span class="inlinecode"><span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">H</span></span>: ... or a hypothesis

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" title="tactic">rewrite</span></span>: use an equality hypothesis (or lemma) to rewrite
        the goal

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" title="tactic">rewrite</span></span> <span class="inlinecode">...</span> <span class="inlinecode"><span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">H</span></span>: ... or a hypothesis

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" title="tactic">symmetry</span></span>: changes a goal of the form <span class="inlinecode"><span class="id" title="var">t</span>=<span class="id" title="var">u</span></span> into <span class="inlinecode"><span class="id" title="var">u</span>=<span class="id" title="var">t</span></span>

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" title="tactic">symmetry</span></span> <span class="inlinecode"><span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">H</span></span>: changes a hypothesis of the form <span class="inlinecode"><span class="id" title="var">t</span>=<span class="id" title="var">u</span></span> into
        <span class="inlinecode"><span class="id" title="var">u</span>=<span class="id" title="var">t</span></span>

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" title="tactic">transitivity</span></span> <span class="inlinecode"><span class="id" title="var">y</span></span>: prove a goal <span class="inlinecode"><span class="id" title="var">x</span>=<span class="id" title="var">z</span></span> by proving two new subgoals,
        <span class="inlinecode"><span class="id" title="var">x</span>=<span class="id" title="var">y</span></span> and <span class="inlinecode"><span class="id" title="var">y</span>=<span class="id" title="var">z</span></span>

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" title="tactic">unfold</span></span>: replace a defined constant by its right-hand side in
        the goal

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" title="tactic">unfold</span>...</span> <span class="inlinecode"><span class="id" title="tactic">in</span></span> <span class="inlinecode"><span class="id" title="var">H</span></span>: ... or a hypothesis

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" title="tactic">destruct</span>...</span> <span class="inlinecode"><span class="id" title="keyword">as</span>...</span>: case analysis on values of inductively
        defined types

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" title="tactic">destruct</span>...</span> <span class="inlinecode"><span class="id" title="var">eqn</span>:...</span>: specify the name of an equation to be
        added to the context, recording the result of the case
        analysis

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" title="tactic">induction</span>...</span> <span class="inlinecode"><span class="id" title="keyword">as</span>...</span>: induction on values of inductively
        defined types

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" title="tactic">injection</span></span>: reason by injectivity on equalities
        between values of inductively defined types

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" title="tactic">discriminate</span></span>: reason by disjointness of constructors on
        equalities between values of inductively defined types

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" title="tactic">assert</span></span> <span class="inlinecode">(<span class="id" title="var">H</span>:</span> <span class="inlinecode"><span class="id" title="var">e</span>)</span> (or <span class="inlinecode"><span class="id" title="tactic">assert</span></span> <span class="inlinecode">(<span class="id" title="var">e</span>)</span> <span class="inlinecode"><span class="id" title="keyword">as</span></span> <span class="inlinecode"><span class="id" title="var">H</span></span>): introduce a "local
        lemma" <span class="inlinecode"><span class="id" title="var">e</span></span> and call it <span class="inlinecode"><span class="id" title="var">H</span></span>

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" title="tactic">generalize</span></span> <span class="inlinecode"><span class="id" title="tactic">dependent</span></span> <span class="inlinecode"><span class="id" title="var">x</span></span>: move the variable <span class="inlinecode"><span class="id" title="var">x</span></span> (and anything
        else that depends on it) from the context back to an explicit
        hypothesis in the goal formula

<div class="paragraph"> </div>


</li>
<li> <span class="inlinecode"><span class="id" title="tactic">f_equal</span></span>: change a goal of the form <span class="inlinecode"><span class="id" title="var">f</span></span> <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">f</span></span> <span class="inlinecode"><span class="id" title="var">y</span></span> into <span class="inlinecode"><span class="id" title="var">x</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" title="var">y</span></span> 
</li>
</ul>

</div>

<div class="doc">
<a id="lab159"></a><h1 class="section">Additional Exercises</h1>

<div class="paragraph"> </div>

<a id="lab160"></a><h4 class="section">Exercise: 3 stars, standard (eqb_sym)</h4>

</div>
<div class="code">
<span class="id" title="keyword">Theorem</span> <a id="eqb_sym" class="idref" href="#eqb_sym"><span class="id" title="lemma">eqb_sym</span></a> : <span class="id" title="keyword">∀</span> (<a id="n:124" class="idref" href="#n:124"><span class="id" title="binder">n</span></a> <a id="m:125" class="idref" href="#m:125"><span class="id" title="binder">m</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>),<br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="Tactics.html#n:124"><span class="id" title="variable">n</span></a> <a class="idref" href="Basics.html#ad2ec4e405f68c46c0a176e3e94ae2e<sub>3</sub>"><span class="id" title="notation">=?</span></a> <a class="idref" href="Tactics.html#m:125"><span class="id" title="variable">m</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="Tactics.html#m:125"><span class="id" title="variable">m</span></a> <a class="idref" href="Basics.html#ad2ec4e405f68c46c0a176e3e94ae2e<sub>3</sub>"><span class="id" title="notation">=?</span></a> <a class="idref" href="Tactics.html#n:124"><span class="id" title="variable">n</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

<a id="lab161"></a><h4 class="section">Exercise: 3 stars, advanced, optional (eqb_sym_informal)</h4>
 Give an informal proof of this lemma that corresponds to your
    formal proof above:

<div class="paragraph"> </div>

   Theorem: For any <span class="inlinecode"><span class="id" title="var">nat</span></span>s <span class="inlinecode"><span class="id" title="var">n</span></span> <span class="inlinecode"><span class="id" title="var">m</span></span>, <span class="inlinecode">(<span class="id" title="var">n</span></span> <span class="inlinecode">=?</span> <span class="inlinecode"><span class="id" title="var">m</span>)</span> <span class="inlinecode">=</span> <span class="inlinecode">(<span class="id" title="var">m</span></span> <span class="inlinecode">=?</span> <span class="inlinecode"><span class="id" title="var">n</span>)</span>.

<div class="paragraph"> </div>

   Proof: 
</div>
<div class="code">
&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

<a id="lab162"></a><h4 class="section">Exercise: 3 stars, standard, optional (eqb_trans)</h4>

</div>
<div class="code">
<span class="id" title="keyword">Theorem</span> <a id="eqb_trans" class="idref" href="#eqb_trans"><span class="id" title="lemma">eqb_trans</span></a> : <span class="id" title="keyword">∀</span> <a id="n:126" class="idref" href="#n:126"><span class="id" title="binder">n</span></a> <a id="m:127" class="idref" href="#m:127"><span class="id" title="binder">m</span></a> <a id="p:128" class="idref" href="#p:128"><span class="id" title="binder">p</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="Tactics.html#n:126"><span class="id" title="variable">n</span></a> <a class="idref" href="Basics.html#ad2ec4e405f68c46c0a176e3e94ae2e<sub>3</sub>"><span class="id" title="notation">=?</span></a> <a class="idref" href="Tactics.html#m:127"><span class="id" title="variable">m</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="Tactics.html#m:127"><span class="id" title="variable">m</span></a> <a class="idref" href="Basics.html#ad2ec4e405f68c46c0a176e3e94ae2e<sub>3</sub>"><span class="id" title="notation">=?</span></a> <a class="idref" href="Tactics.html#p:128"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="Tactics.html#n:126"><span class="id" title="variable">n</span></a> <a class="idref" href="Basics.html#ad2ec4e405f68c46c0a176e3e94ae2e<sub>3</sub>"><span class="id" title="notation">=?</span></a> <a class="idref" href="Tactics.html#p:128"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

<a id="lab163"></a><h4 class="section">Exercise: 3 stars, advanced (split_combine)</h4>
 We proved, in an exercise above, that for all lists of pairs,
    <span class="inlinecode"><span class="id" title="var">combine</span></span> is the inverse of <span class="inlinecode"><span class="id" title="tactic">split</span></span>.  How would you formalize the
    statement that <span class="inlinecode"><span class="id" title="tactic">split</span></span> is the inverse of <span class="inlinecode"><span class="id" title="var">combine</span></span>?  When is this
    property true?

<div class="paragraph"> </div>

    Complete the definition of <span class="inlinecode"><span class="id" title="var">split_combine_statement</span></span> below with a
    property that states that <span class="inlinecode"><span class="id" title="tactic">split</span></span> is the inverse of
    <span class="inlinecode"><span class="id" title="var">combine</span></span>. Then, prove that the property holds. (Be sure to leave
    your induction hypothesis general by not doing <span class="inlinecode"><span class="id" title="tactic">intros</span></span> on more
    things than necessary.  Hint: what property do you need of <span class="inlinecode"><span class="id" title="var">l<sub>1</sub></span></span>
    and <span class="inlinecode"><span class="id" title="var">l<sub>2</sub></span></span> for <span class="inlinecode"><span class="id" title="tactic">split</span></span> <span class="inlinecode">(<span class="id" title="var">combine</span></span> <span class="inlinecode"><span class="id" title="var">l<sub>1</sub></span></span> <span class="inlinecode"><span class="id" title="var">l<sub>2</sub></span>)</span> <span class="inlinecode">=</span> <span class="inlinecode">(<span class="id" title="var">l<sub>1</sub></span>,<span class="id" title="var">l<sub>2</sub></span>)</span> to be true?) 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Definition</span> <a id="split_combine_statement" class="idref" href="#split_combine_statement"><span class="id" title="definition">split_combine_statement</span></a> : <span class="id" title="keyword">Prop</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;("<span class="inlinecode">:</span> <span class="inlinecode"><span class="id" title="keyword">Prop</span></span>"&nbsp;means&nbsp;that&nbsp;we&nbsp;are&nbsp;giving&nbsp;a&nbsp;name&nbsp;to&nbsp;a<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;logical&nbsp;proposition&nbsp;here.)&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;REPLACE&nbsp;THIS&nbsp;LINE&nbsp;WITH&nbsp;":=&nbsp;_your_definition_&nbsp;."&nbsp;*)</span>. <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Theorem</span> <a id="split_combine" class="idref" href="#split_combine"><span class="id" title="lemma">split_combine</span></a> : <a class="idref" href="Tactics.html#split_combine_statement"><span class="id" title="axiom">split_combine_statement</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;Do&nbsp;not&nbsp;modify&nbsp;the&nbsp;following&nbsp;line:&nbsp;*)</span><br/>
<span class="id" title="keyword">Definition</span> <a id="manual_grade_for_split_combine" class="idref" href="#manual_grade_for_split_combine"><span class="id" title="definition">manual_grade_for_split_combine</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> (<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a><a class="idref" href="Poly.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">×</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) := <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

<a id="lab164"></a><h4 class="section">Exercise: 3 stars, advanced (filter_exercise)</h4>
 This one is a bit challenging.  Pay attention to the form of your
    induction hypothesis. 
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Theorem</span> <a id="filter_exercise" class="idref" href="#filter_exercise"><span class="id" title="lemma">filter_exercise</span></a> : <span class="id" title="keyword">∀</span> (<a id="X:129" class="idref" href="#X:129"><span class="id" title="binder">X</span></a> : <span class="id" title="keyword">Type</span>) (<a id="test:130" class="idref" href="#test:130"><span class="id" title="binder">test</span></a> : <a class="idref" href="Tactics.html#X:129"><span class="id" title="variable">X</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Basics.html#bool"><span class="id" title="inductive">bool</span></a>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<a id="x:131" class="idref" href="#x:131"><span class="id" title="binder">x</span></a> : <a class="idref" href="Tactics.html#X:129"><span class="id" title="variable">X</span></a>) (<a id="l:132" class="idref" href="#l:132"><span class="id" title="binder">l</span></a> <a id="lf:133" class="idref" href="#lf:133"><span class="id" title="binder">lf</span></a> : <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Tactics.html#X:129"><span class="id" title="variable">X</span></a>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Poly.html#filter"><span class="id" title="definition">filter</span></a> <a class="idref" href="Tactics.html#test:130"><span class="id" title="variable">test</span></a> <a class="idref" href="Tactics.html#l:132"><span class="id" title="variable">l</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Tactics.html#x:131"><span class="id" title="variable">x</span></a> <a class="idref" href="Poly.html#:::x_'::'_x"><span class="id" title="notation">::</span></a> <a class="idref" href="Tactics.html#lf:133"><span class="id" title="variable">lf</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Tactics.html#test:130"><span class="id" title="variable">test</span></a> <a class="idref" href="Tactics.html#x:131"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

<a id="lab165"></a><h4 class="section">Exercise: 4 stars, advanced, especially useful (forall_exists_challenge)</h4>
 Define two recursive <span class="inlinecode"><span class="id" title="var">Fixpoints</span></span>, <span class="inlinecode"><span class="id" title="var">forallb</span></span> and <span class="inlinecode"><span class="id" title="var">existsb</span></span>.  The
    first checks whether every element in a list satisfies a given
    predicate:
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">forallb</span> <span class="id" title="var">oddb</span> [1;3;5;7;9] = <span class="id" title="var">true</span><br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">forallb</span> <span class="id" title="var">negb</span> [<span class="id" title="var">false</span>;<span class="id" title="var">false</span>] = <span class="id" title="var">true</span><br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">forallb</span> <span class="id" title="var">evenb</span> [0;2;4;5] = <span class="id" title="var">false</span><br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">forallb</span> (<span class="id" title="var">eqb</span> 5) [] = <span class="id" title="var">true</span>
<div class="paragraph"> </div>

</span>    The second checks whether there exists an element in the list that
    satisfies a given predicate:
<br/>
<span class="inlinecode">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">existsb</span> (<span class="id" title="var">eqb</span> 5) [0;2;3;6] = <span class="id" title="var">false</span><br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">existsb</span> (<span class="id" title="var">andb</span> <span class="id" title="var">true</span>) [<span class="id" title="var">true</span>;<span class="id" title="var">true</span>;<span class="id" title="var">false</span>] = <span class="id" title="var">true</span><br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">existsb</span> <span class="id" title="var">oddb</span> [1;0;0;0;0;3] = <span class="id" title="var">true</span><br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">existsb</span> <span class="id" title="var">evenb</span> [] = <span class="id" title="var">false</span>
<div class="paragraph"> </div>

</span>    Next, define a <i>nonrecursive</i> version of <span class="inlinecode"><span class="id" title="var">existsb</span></span> -- call it
    <span class="inlinecode"><span class="id" title="var">existsb'</span></span> -- using <span class="inlinecode"><span class="id" title="var">forallb</span></span> and <span class="inlinecode"><span class="id" title="var">negb</span></span>.

<div class="paragraph"> </div>

    Finally, prove a theorem <span class="inlinecode"><span class="id" title="var">existsb_existsb'</span></span> stating that
    <span class="inlinecode"><span class="id" title="var">existsb'</span></span> and <span class="inlinecode"><span class="id" title="var">existsb</span></span> have the same behavior.

</div>
<div class="code">

<br/>
<span class="id" title="keyword">Fixpoint</span> <a id="forallb" class="idref" href="#forallb"><span class="id" title="definition">forallb</span></a> {<a id="X:134" class="idref" href="#X:134"><span class="id" title="binder">X</span></a> : <span class="id" title="keyword">Type</span>} (<a id="test:135" class="idref" href="#test:135"><span class="id" title="binder">test</span></a> : <a class="idref" href="Tactics.html#X:134"><span class="id" title="variable">X</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Basics.html#bool"><span class="id" title="inductive">bool</span></a>) (<a id="l:136" class="idref" href="#l:136"><span class="id" title="binder">l</span></a> : <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Tactics.html#X:134"><span class="id" title="variable">X</span></a>) : <a class="idref" href="Basics.html#bool"><span class="id" title="inductive">bool</span></a><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;REPLACE&nbsp;THIS&nbsp;LINE&nbsp;WITH&nbsp;":=&nbsp;_your_definition_&nbsp;."&nbsp;*)</span>. <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="test_forallb_1" class="idref" href="#test_forallb_1"><span class="id" title="definition">test_forallb_1</span></a> : <a class="idref" href="Tactics.html#forallb"><span class="id" title="axiom">forallb</span></a> <a class="idref" href="Basics.html#oddb"><span class="id" title="definition">oddb</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>1<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>3<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>5<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>7<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>9<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a>.<br/>
<span class="id" title="keyword">Proof</span>. <span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="test_forallb_2" class="idref" href="#test_forallb_2"><span class="id" title="definition">test_forallb_2</span></a> : <a class="idref" href="Tactics.html#forallb"><span class="id" title="axiom">forallb</span></a> <a class="idref" href="Basics.html#negb"><span class="id" title="definition">negb</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Basics.html#false"><span class="id" title="constructor">false</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a><a class="idref" href="Basics.html#false"><span class="id" title="constructor">false</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a>.<br/>
<span class="id" title="keyword">Proof</span>. <span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="test_forallb_3" class="idref" href="#test_forallb_3"><span class="id" title="definition">test_forallb_3</span></a> : <a class="idref" href="Tactics.html#forallb"><span class="id" title="axiom">forallb</span></a> <a class="idref" href="Basics.html#evenb"><span class="id" title="definition">evenb</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>0<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>2<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>4<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>5<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Basics.html#false"><span class="id" title="constructor">false</span></a>.<br/>
<span class="id" title="keyword">Proof</span>. <span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="test_forallb_4" class="idref" href="#test_forallb_4"><span class="id" title="definition">test_forallb_4</span></a> : <a class="idref" href="Tactics.html#forallb"><span class="id" title="axiom">forallb</span></a> (<a class="idref" href="Basics.html#eqb"><span class="id" title="definition">eqb</span></a> 5) <a class="idref" href="Poly.html#2c60282cbb04e070c60ae01e76f3865a"><span class="id" title="notation">[]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a>.<br/>
<span class="id" title="keyword">Proof</span>. <span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Fixpoint</span> <a id="existsb" class="idref" href="#existsb"><span class="id" title="definition">existsb</span></a> {<a id="X:138" class="idref" href="#X:138"><span class="id" title="binder">X</span></a> : <span class="id" title="keyword">Type</span>} (<a id="test:139" class="idref" href="#test:139"><span class="id" title="binder">test</span></a> : <a class="idref" href="Tactics.html#X:138"><span class="id" title="variable">X</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Basics.html#bool"><span class="id" title="inductive">bool</span></a>) (<a id="l:140" class="idref" href="#l:140"><span class="id" title="binder">l</span></a> : <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Tactics.html#X:138"><span class="id" title="variable">X</span></a>) : <a class="idref" href="Basics.html#bool"><span class="id" title="inductive">bool</span></a><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;REPLACE&nbsp;THIS&nbsp;LINE&nbsp;WITH&nbsp;":=&nbsp;_your_definition_&nbsp;."&nbsp;*)</span>. <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="test_existsb_1" class="idref" href="#test_existsb_1"><span class="id" title="definition">test_existsb_1</span></a> : <a class="idref" href="Tactics.html#existsb"><span class="id" title="axiom">existsb</span></a> (<a class="idref" href="Basics.html#eqb"><span class="id" title="definition">eqb</span></a> 5) <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>0<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>2<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>3<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>6<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Basics.html#false"><span class="id" title="constructor">false</span></a>.<br/>
<span class="id" title="keyword">Proof</span>. <span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="test_existsb_2" class="idref" href="#test_existsb_2"><span class="id" title="definition">test_existsb_2</span></a> : <a class="idref" href="Tactics.html#existsb"><span class="id" title="axiom">existsb</span></a> (<a class="idref" href="Basics.html#andb"><span class="id" title="definition">andb</span></a> <a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a>) <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a><a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a><a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a><a class="idref" href="Basics.html#false"><span class="id" title="constructor">false</span></a><a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a>.<br/>
<span class="id" title="keyword">Proof</span>. <span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="test_existsb_3" class="idref" href="#test_existsb_3"><span class="id" title="definition">test_existsb_3</span></a> : <a class="idref" href="Tactics.html#existsb"><span class="id" title="axiom">existsb</span></a> <a class="idref" href="Basics.html#oddb"><span class="id" title="definition">oddb</span></a> <a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">[</span></a>1<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>0<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>0<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>0<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>0<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">;</span></a>3<a class="idref" href="Poly.html#fa57d319973f6d58544a8887d0d48ea<sub>6</sub>"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Basics.html#true"><span class="id" title="constructor">true</span></a>.<br/>
<span class="id" title="keyword">Proof</span>. <span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="test_existsb_4" class="idref" href="#test_existsb_4"><span class="id" title="definition">test_existsb_4</span></a> : <a class="idref" href="Tactics.html#existsb"><span class="id" title="axiom">existsb</span></a> <a class="idref" href="Basics.html#evenb"><span class="id" title="definition">evenb</span></a> <a class="idref" href="Poly.html#2c60282cbb04e070c60ae01e76f3865a"><span class="id" title="notation">[]</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Basics.html#false"><span class="id" title="constructor">false</span></a>.<br/>
<span class="id" title="keyword">Proof</span>. <span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Definition</span> <a id="existsb'" class="idref" href="#existsb'"><span class="id" title="definition">existsb'</span></a> {<a id="X:142" class="idref" href="#X:142"><span class="id" title="binder">X</span></a> : <span class="id" title="keyword">Type</span>} (<a id="test:143" class="idref" href="#test:143"><span class="id" title="binder">test</span></a> : <a class="idref" href="Tactics.html#X:142"><span class="id" title="variable">X</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Basics.html#bool"><span class="id" title="inductive">bool</span></a>) (<a id="l:144" class="idref" href="#l:144"><span class="id" title="binder">l</span></a> : <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Tactics.html#X:142"><span class="id" title="variable">X</span></a>) : <a class="idref" href="Basics.html#bool"><span class="id" title="inductive">bool</span></a><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;REPLACE&nbsp;THIS&nbsp;LINE&nbsp;WITH&nbsp;":=&nbsp;_your_definition_&nbsp;."&nbsp;*)</span>. <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Theorem</span> <a id="existsb_existsb'" class="idref" href="#existsb_existsb'"><span class="id" title="lemma">existsb_existsb'</span></a> : <span class="id" title="keyword">∀</span> (<a id="X:145" class="idref" href="#X:145"><span class="id" title="binder">X</span></a> : <span class="id" title="keyword">Type</span>) (<a id="test:146" class="idref" href="#test:146"><span class="id" title="binder">test</span></a> : <a class="idref" href="Tactics.html#X:145"><span class="id" title="variable">X</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Basics.html#bool"><span class="id" title="inductive">bool</span></a>) (<a id="l:147" class="idref" href="#l:147"><span class="id" title="binder">l</span></a> : <a class="idref" href="Poly.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="Tactics.html#X:145"><span class="id" title="variable">X</span></a>),<br/>
&nbsp;&nbsp;<a class="idref" href="Tactics.html#existsb"><span class="id" title="axiom">existsb</span></a> <a class="idref" href="Tactics.html#test:146"><span class="id" title="variable">test</span></a> <a class="idref" href="Tactics.html#l:147"><span class="id" title="variable">l</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Tactics.html#existsb'"><span class="id" title="axiom">existsb'</span></a> <a class="idref" href="Tactics.html#test:146"><span class="id" title="variable">test</span></a> <a class="idref" href="Tactics.html#l:147"><span class="id" title="variable">l</span></a>.<br/>
<span class="id" title="keyword">Proof</span>. <span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="code">

<br/>
<span class="comment">(*&nbsp;2020-08-24&nbsp;15:39&nbsp;*)</span><br/>
</div>
</div>

<div id="footer">
<hr/><a href="coqindex.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a>
</div>

</div>

</body>
</html>